Theorem CommGroup.torsion_eq_top_iff

Modification history

2026-07-24 18:27

Mathlib/GroupTheory/Torsion.lean

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

Modified CommGroup.torsion_eq_top_iff View on Github →

2026-05-10 10:59

Mathlib/GroupTheory/Torsion.lean

feat(GroupTheory/Torsion): add `torsion_eq_top_iff` (#38718) …

Added CommGroup.torsion_eq_top_iff View on Github →