Commit 2023-12-22 10:33 98067b25

feat(LinearAlgebra/Dimension): add various surjective_injective results (#9156) Add various results concerning modules M / R and M' / R' with maps i : R -> R' and j : M -> M' which are compatible with scalar multiplications on M and M'.

• if i : R' -> R is injective and j is injective, then:
  • LinearIndependent.map_of_injective_injective: j preserves linear independent subsets.
  • [lift_]rank_le_of_injective_injective: rank of M / R is smaller than or equal to the rank of M' / R'.
• if i is surjective and j is injective, then:
  • LinearIndependent.map_of_surjective_injective: j preserves linear independent subsets.
  • [lift_]rank_le_of_surjective_injective: rank of M / R is smaller than or equal to the rank of M' / R'.
• if i and j are both bijective, then [lift_]rank_eq_of_equiv_equiv: rank of M / R is equal to the rank of M' / R'. Also add the Algebra versions of these results.