Results relating rank and torsion.

theorem Module.IsTorsion.rank_eq_zero {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] (h : IsTorsion R M) : Module.rank R M = 0

A torsion module has rank zero.

theorem Module.IsTorsion.finrank_eq_zero {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] (h : IsTorsion R M) : finrank R M = 0

theorem Module.rank_eq_zero_iff_isTorsion {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] : Module.rank R M = 0 ↔ IsTorsion R M

@[deprecated Module.rank_eq_zero_iff_isTorsion (since := "2026-07-14")]

theorem rank_eq_zero_iff_isTorsion {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] : Module.rank R M = 0 ↔ Module.IsTorsion R M

Alias of Module.rank_eq_zero_iff_isTorsion.

theorem Module.finrank_eq_zero_iff_isTorsion {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] : finrank R M = 0 ↔ IsTorsion R M

The StrongRankCondition is automatic. See commRing_strongRankCondition.