Theorem IsMulTorsionFree.zpow_right_inj

Modification history

2026-10-17 09:16
Mathlib/Algebra/Group/Torsion.lean
feat(Algebra): add zpow_right_injective (#42914) …
Added IsMulTorsionFree.zpow_right_injView on Github →