mathlib3

4cf7ca0e - chore(linear_algebra/free_module/finite/rank): move lemmas from `module.free` to `finite_dimensional` (#18733)

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](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/naming.3A.20finrank.20and.20rank.20lemmas/near/346701602)