Theorem Module.IsTorsion.finrank_eq_zero

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.IsTorsion.finrank_eq_zeroView on Github →