Theorem IsMulTorsionFree.pow_right_injective

Modification history

2026-10-17 09:16
Mathlib/Algebra/Group/Torsion.lean
feat(Algebra): add zpow_right_injective (#42914) …
Modified IsMulTorsionFree.pow_right_injectiveView on Github →
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 →