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] : finrank R M = 0 ↔ IsTorsion R M

The StrongRankCondition is automatic. See commRing_strongRankCondition.