Commit 2023-04-05 10:55 039a089d

refactor(linear_algebra/dimension): use rank in lemma names instead of dim (#18741) The dim name is left from the previous name of the function, vector_space.dim. When that was merged with module.rank in #7322, we left renaming the existing lemmas as future work. This commit was made by replacing (\b|(?<=_))dim(\b|(?=_)) with rank in the dimension and finite_dimensional files, and then manually fixing downstream breakages; it's important not to rename power_basis.dim at the same time! Deciding whether to move some of these to the module namespace is left as future work, the diff is already big enough.