Rank and torsion

Main statements

• rank_quotient_eq_of_le_torsion : rank M/N = rank M if N ≤ torsion M.
• finrank_quotient_eq_of_le_torsion : finrank M/N = finrank M if N ≤ torsion M.
• finrank_quotient_torsion_eq : finrank ℤ (M / torsion M) = finrank ℤ M for an additive commutative group 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

theorem finrank_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.finrank R (M ⧸ M') = Module.finrank R M

theorem finrank_quotient_torsion_eq {M : Type u_1} [AddCommGroup M] : Module.finrank ℤ (M ⧸ AddSubgroup.toIntSubmodule (AddCommGroup.torsion M)) = Module.finrank ℤ M

Quotienting an additive commutative group by its torsion subgroup does not change its ℤ-finrank.