Commit 2023-04-04 11:37 4cf7ca0e

chore(linear_algebra/free_module/finite/rank): move lemmas from module.free to finite_dimensional (#18733) The lemmas about finite-dimensional spaces are currently scattered between namespaces. This commit mostly addresses the confusion by renaming all the module.free.finrank_* lemmas to finite_dimensional.finrank_*. This rename makes it apparent that finrank_eq_dim and finrank_eq_rank are duplicates; though it seems that for performances reasons it's still useful in one or two places to keep both. Zulip thread