Commit 2026-10-17 09:16 96bc85d5

feat(Algebra): add zpow_right_injective (#42914) Add IsMulTorsionFree.zpow_right_injective_iff, its injectivity alias, and the _inj version, together with their additive counterparts via to_additive. Move the natural power injectivity lemmas from Mathlib.Algebra.Ring.NonZeroDivisors to Mathlib.Algebra.Group.Torsion and add their additive counterparts via to_additive. Use natural scalar injectivity to move CharZero.of_hasUniqueDiv and its deprecated alias CharZero.of_isAddTorsionFree from Mathlib.Algebra.Module.Torsion.Free to Mathlib.Algebra.Module.NatInt, weakening AddCommGroup M to AddCancelCommMonoid M.