Theorem 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) …
Deleted rank_eq_zero_iff_isTorsionView on Github →
2025-07-08 11:58
Mathlib/LinearAlgebra/Dimension/Torsion/Finite.lean
chore: whitespace fixes in lemmas (#26892) …
Added rank_eq_zero_iff_isTorsionView on Github →
2024-12-09 19:23
Mathlib/LinearAlgebra/Dimension/Torsion/Finite.lean
chore: simplify variables in LinearAlgebra.Dimension.Torsion.Finite (#19839)
Deleted rank_eq_zero_iff_isTorsionView on Github →
2024-12-09 12:57
Mathlib/LinearAlgebra/Dimension/Finite.lean
chore: don't need group-theoretic exponent to set up finite dimensional vector spaces (#19827)
Modified rank_eq_zero_iff_isTorsionView on Github →
2024-01-01 14:48
Mathlib/LinearAlgebra/Dimension.lean
chore: Reorganize results about `rank` and `finrank`. (#9349) …
Modified rank_eq_zero_iff_isTorsionView on Github →
2023-12-18 12:58
Mathlib/LinearAlgebra/Dimension.lean
chore: Generalize results on `finrank` to rings. (#8912) …
Added rank_eq_zero_iff_isTorsionView on Github →