Rank and torsion

Main statements

• rank_quotient_eq_of_le_torsion : rank M/N = rank M if N ≤ torsion M.

theorem rank_quotient_eq_of_le_torsion {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {M' : Submodule R M} (hN : M' ≤ Submodule.torsion R M) : Module.rank R (M ⧸ M') = Module.rank R M