Theorem IsMulTorsionFree.pow_eq_one_iff

Modification history

2025-10-27 08:05
Mathlib/Algebra/Group/Torsion.lean
feat(Algebra/Group/Torsion): characterise when `a ^ n = 1` (#30680)
Modified IsMulTorsionFree.pow_eq_one_iffView on Github →
2025-09-01 13:46
Mathlib/Algebra/Group/Torsion.lean
feat(DedekindDomain): Monoid of ideals is torsion-free (#28169) …
Added IsMulTorsionFree.pow_eq_one_iffView on Github →