Theorem CommGroup.freeRank_eq_zero

Modification history

2026-07-24 18:27

Mathlib/GroupTheory/Torsion.lean

chore(GroupTheory/Torsion): rename `IsTorsion` to `IsMulTorsion` (#41213) …

Modified CommGroup.freeRank_eq_zero View on Github →

2026-06-01 18:16

Mathlib/GroupTheory/Torsion.lean

feat(GroupTheory/Torsion): the free rank of an abelian group (#39972) …

Added CommGroup.freeRank_eq_zero View on Github →