Commit 2025-10-27 08:05 747d81a5

View on Github →

feat(Algebra/Group/Torsion): characterise when a ^ n = 1 (#30680)

Estimated changes

Modified Mathlib/Algebra/Group/Torsion.lean

deleted theorem IsMulTorsionFree.pow_eq_one_iff'

modified theorem IsMulTorsionFree.pow_eq_one_iff

added theorem IsMulTorsionFree.pow_eq_one_iff_left

added theorem IsMulTorsionFree.pow_eq_one_iff_right

added theorem IsMulTorsionFree.zpow_eq_one_iff

added theorem IsMulTorsionFree.zpow_eq_one_iff_left

added theorem IsMulTorsionFree.zpow_eq_one_iff_right

modified theorem sq_eq_one

Modified Mathlib/Algebra/GroupWithZero/Torsion.lean

Modified Mathlib/Algebra/Ring/NonZeroDivisors.lean