Commit 2025-09-12 16:37 c4611fa3

View on Github →

feat(IsMulTorsionFree): the power map of a nontrivial regular element is injective (#28738)

Estimated changes

Modified Mathlib/Algebra/Group/Opposite.lean

Modified Mathlib/Algebra/Group/Torsion.lean

added theorem IsMulTorsionFree.pow_eq_one_iff'

Modified Mathlib/Algebra/Ring/NonZeroDivisors.lean

added theorem IsLeftRegular.pow_injective

added theorem IsMulTorsionFree.pow_right_inj

added theorem IsMulTorsionFree.pow_right_injective

added theorem IsMulTorsionFree.pow_right_injective₀

added theorem IsMulTorsionFree.pow_right_inj₀

added theorem IsRightRegular.pow_injective

modified theorem isRegular_iff_isUnit_of_finite