Commit 2023-04-04 11:37 be2ac64b
View on Github →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.