feat(Algebra/Group/Torsion): characterise when a ^ n = 1 (#30680)

Author: YaelDillies

Mathlib/Algebra/Group/Torsion.lean

@@ -35,19 +35,27 @@ lemma pow_left_injective (hn : n ≠ 0) : Injective fun a : M ↦ a ^ n :=
 @[to_additive nsmul_right_inj]
 lemma pow_left_inj (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := (pow_left_injective hn).eq_iff
 
-@[to_additive]
-lemma IsMulTorsionFree.pow_eq_one_iff (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 :=
-  ⟨fun h ↦ by rwa [← pow_left_inj hn, one_pow], fun h ↦ by rw [h, one_pow]⟩
+@[to_additive IsAddTorsionFree.nsmul_eq_zero_iff_right]
+lemma IsMulTorsionFree.pow_eq_one_iff_left (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 := by
+  rw [← pow_left_inj (a := a) hn, one_pow]
 
-@[to_additive]
-lemma IsMulTorsionFree.pow_eq_one_iff' (ha : a ≠ 1) : a ^ n = 1 ↔ n = 0 := by
-  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, pow_zero]⟩
-  by_contra h'
-  simpa [h] using (pow_left_injective h').ne ha
+-- We want to use `IsAddTorsion.nsmul_eq_zero_iff` earlier than `smul_eq_zero`.
+@[to_additive (attr := simp high)]
+lemma IsMulTorsionFree.pow_eq_one_iff : a ^ n = 1 ↔ a = 1 ∨ n = 0 := by
+  obtain rfl | hn := eq_or_ne n 0 <;> simp [pow_eq_one_iff_left, *]
+
+@[to_additive IsAddTorsionFree.nsmul_eq_zero_iff_left]
+lemma IsMulTorsionFree.pow_eq_one_iff_right (ha : a ≠ 1) : a ^ n = 1 ↔ n = 0 := by simp [*]
+
+@[deprecated (since := "2025-10-19")]
+alias IsAddTorsionFree.nsmul_eq_zero_iff' := IsAddTorsionFree.nsmul_eq_zero_iff_left
+
+@[deprecated (since := "2025-10-19")]
+alias IsMulTorsionFree.pow_eq_one_iff' := IsMulTorsionFree.pow_eq_one_iff_right
 
 /-- See `sq_eq_one_iff` for a version that holds in rings. -/
 @[to_additive two_nsmul_eq_zero]
-lemma sq_eq_one : a ^ 2 = 1 ↔ a = 1 := IsMulTorsionFree.pow_eq_one_iff (by cutsat)
+lemma sq_eq_one : a ^ 2 = 1 ↔ a = 1 := IsMulTorsionFree.pow_eq_one_iff_left (by cutsat)
 
 end Monoid
 
@@ -69,6 +77,18 @@ lemma zpow_left_inj (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := (zpow_left_injec
 and `zsmul_lt_zsmul_iff'`. -/]
 lemma zpow_eq_zpow_iff' (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := zpow_left_inj hn
 
+@[to_additive IsAddTorsionFree.zsmul_eq_zero_iff_right]
+lemma IsMulTorsionFree.zpow_eq_one_iff_left (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 := by
+  rw [← zpow_left_inj (a := a) hn, one_zpow]
+
+-- We want to use `IsAddTorsion.zsmul_eq_zero_iff` earlier than `smul_eq_zero`.
+@[to_additive (attr := simp high)]
+lemma IsMulTorsionFree.zpow_eq_one_iff : a ^ n = 1 ↔ a = 1 ∨ n = 0 := by
+  obtain rfl | hn := eq_or_ne n 0 <;> simp [zpow_eq_one_iff_left, *]
+
+@[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] 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/GroupWithZero/Torsion.lean

@@ -37,7 +37,7 @@ instance : IsMulTorsionFree M := by
       ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this
   replace hx : IsLeftRegular (x ^ n) := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hx).pow n
   rw [← hu, mul_pow, eq_comm, IsLeftRegular.mul_left_eq_self_iff hx, ← Units.val_pow_eq_pow_val,
-    Units.val_eq_one, IsMulTorsionFree.pow_eq_one_iff hn] at hxy
+    Units.val_eq_one, IsMulTorsionFree.pow_eq_one_iff_left hn] at hxy
   rwa [hxy, Units.val_one, mul_one] at hu
 
 end UniqueFactorizationMonoid

Mathlib/Algebra/Ring/NonZeroDivisors.lean

@@ -27,7 +27,7 @@ theorem IsLeftRegular.pow_injective [IsMulTorsionFree R]
   have main {n m} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m) : n = m := by
     obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le h₁
     rw [pow_add, eq_comm, IsLeftRegular.mul_left_eq_self_iff (hx.pow n),
-      IsMulTorsionFree.pow_eq_one_iff' hx'] at h₂
+      IsMulTorsionFree.pow_eq_one_iff_right hx'] at h₂
     rw [h₂, Nat.add_zero]
   obtain h | h := Nat.le_or_le n m
   · exact main h hnm