Theorem IsMulTorsionFree.pow_right_inj₀

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_inj₀View on Github →