Theorem IsMulTorsionFree.zpow_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)
Added IsMulTorsionFree.zpow_eq_one_iffView on Github →