mathlib

039a089d - refactor(linear_algebra/dimension): use `rank` in lemma names instead of `dim` (#18741)

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.