mathlib3

e95e4f92 - feat(linear_algebra/finite_dimensional): generalize results to `module.finite` (#18811)

feat(linear_algebra/finite_dimensional): generalize results to `module.finite` (#18811) This generalize the following from `finite_dimensional` over division rings to `module.finite` over free modules: * `finite_dimensional.nonempty_linear_equiv_of_finrank_eq` (moved from `nonempty_linear_equiv_of_finrank_eq`) * `finite_dimensional.nonempty_linear_equiv_iff_finrank_eq` (moved from `nonempty_linear_equiv_iff_finrank_eq`) * `linear_equiv.of_finrank_eq` * `module.finite.map` (moved from `finite_dimensional.submodule.map.finite_dimensional`). This is the only lemma moved across the porting tide. * `submodule.finrank_map_le` (moved from `finite_dimensional.finrank_map_le`) * `submodule.finrank_map_subtype_eq` (moved from `finite_dimensional.finrank_map_subtype_eq`, needs no finite or free assumptions at all) * `submodule.finrank_le_finrank_of_le`