Theorem IsMulTorsionFree.pow_eq_one_iff'

Modification history

2025-09-12 16:37
Mathlib/Algebra/Group/Torsion.lean
feat(IsMulTorsionFree): the power map of a nontrivial regular element is injective (#28738)
Added IsMulTorsionFree.pow_eq_one_iff'View on Github →