mathlib

be2ac64b - chore(linear_algebra/dimension): rename `rank` to `linear_map.rank` (#18734)

chore(linear_algebra/dimension): rename `rank` to `linear_map.rank` (#18734) It's a bit weird having `rank` in the root namespace, defined in terms of `module.rank` which isn't. This moves all the lemmas into a single block at the end of the file, as they were previously spread through the file.