feat(Algebra): add zpow_right_injective

Mathlib/Algebra/Group/Torsion.lean

@@ -87,6 +87,14 @@ lemma IsMulTorsionFree.zpow_eq_one_iff : a ^ n = 1 ↔ a = 1 ∨ n = 0 := by
 @[to_additive IsAddTorsionFree.zsmul_eq_zero_iff_left]
 lemma IsMulTorsionFree.zpow_eq_one_iff_right (ha : a ≠ 1) : a ^ n = 1 ↔ n = 0 := by simp [*]
 
+@[to_additive zsmul_left_injective]
+lemma zpow_right_injective (ha : a ≠ 1) :
+    (a ^ · : ℤ → G).Injective := by
+  intro m n h
+  apply Int.sub_eq_zero.mp
+  apply (IsMulTorsionFree.zpow_eq_one_iff_right ha).mp
+  simp [zpow_sub, h]
+
 @[to_additive] lemma self_eq_inv : a = a⁻¹ ↔ a = 1 := by rw [← sq_eq_one, sq, mul_eq_one_iff_eq_inv]
 @[to_additive] lemma inv_eq_self : a⁻¹ = a ↔ a = 1 := by rw [eq_comm, self_eq_inv]
 @[to_additive] lemma self_ne_inv : a ≠ a⁻¹ ↔ a ≠ 1 := self_eq_inv.ne

Mathlib/Algebra/Module/NatInt.lean

@@ -207,6 +207,16 @@ instance AddCommGroup.intIsScalarTower {R : Type u} {M : Type v} [Ring R] [AddCo
     | ofNat => simp [mul_smul, Nat.cast_smul_eq_nsmul]
     | negSucc => simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]
 
+variable (R M) in
+/-- Only a ring of characteristic zero can have a non-trivial module without additive or
+scalar torsion. -/
+lemma CharZero.of_isAddTorsionFree [Semiring R] [AddCommGroup M] [Module R M]
+    [Nontrivial M] [IsAddTorsionFree M] : CharZero R := by
+  refine ⟨fun {n m h} ↦ ?_⟩
+  obtain ⟨x, hx⟩ := exists_ne (0 : M)
+  replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h]
+  simpa using zsmul_left_injective hx h
+
 variable (M) in
 /-- If `M` is an `R`-module with one and `M` has characteristic zero, then `R` has characteristic
 zero as well. Usually `M` is an `R`-algebra. -/

Mathlib/Algebra/Module/Torsion/Free.lean

@@ -177,17 +177,3 @@ lemma smul_left_injective (hm : m ≠ 0) : ((· • m) : R → M).Injective := b
   (smul_left_injective _ hm).eq_iff
 
 end Ring
-
-section Semiring
-variable (R M) [Semiring R] [AddCommGroup M] [Module R M]
-
--- TODO: Add a `ℤ`-specific version of `smul_left_injective` and move this lemma to an earlier file.
-/-- Only a ring of characteristic zero can have a non-trivial module without additive or
-scalar torsion. -/
-lemma CharZero.of_isAddTorsionFree [Nontrivial M] [IsAddTorsionFree M] : CharZero R := by
-  refine ⟨fun {n m h} ↦ ?_⟩
-  obtain ⟨x, hx⟩ := exists_ne (0 : M)
-  replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h]
-  simpa using smul_left_injective ℤ hx h
-
-end Semiring