Commit 2023-04-14 22:49 e95e4f92

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