Theorem IsLeftRegular.pow_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 IsLeftRegular.pow_injectiveView on Github →