Theorem IsMulTorsionFree.pow_right_injective

Modification history

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