Theorem Module.rank_eq_zero_iff_isTorsion

Modification history

2026-07-14 19:17
Mathlib/LinearAlgebra/Dimension/Torsion/Finite.lean
chore(LinearAlgebra/Dimension/Torsion/Finite): a torsion module has rank zero (#41739) …
Added Module.rank_eq_zero_iff_isTorsionView on Github →