Results relating rank and torsion. #
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
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]
:
Module.finrank R M = 0 ↔ Module.IsTorsion R M
The StrongRankCondition is automatic. See commRing_strongRankCondition.