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)

Deleted IsMulTorsionFree.pow_eq_one_iff'View on Github →

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 →