refactor: unify the two versions of pow_eq_one_iff (leanprover-community#30799)

One version is about torsion-free monoids, the other one about linearly ordered monoids. I argue that all linearly ordered monoids of interest are torsion-free, and therefore the correct lemma to keep is the former.

As a byproduct, I must move a few `MonoidHom` lemmas.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Should.20linear.20ordered.20comm.20monoids.20with.20zero.20be.20torsion-free)

Author: YaelDillies

Mathlib/Algebra/Group/Torsion.lean

@@ -39,27 +39,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 IsAddTorsionFree.nsmul_eq_zero_iff_right]
-lemma IsMulTorsionFree.pow_eq_one_iff_left (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 := by
+@[to_additive nsmul_eq_zero_iff_right]
+lemma pow_eq_one_iff_left (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 := by
   rw [← pow_left_inj (a := a) hn, one_pow]
 
 -- 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
+lemma 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 [*]
+@[to_additive nsmul_eq_zero_iff_left]
+lemma 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
+alias IsAddTorsionFree.nsmul_eq_zero_iff' := nsmul_eq_zero_iff_left
 
 @[deprecated (since := "2025-10-19")]
-alias IsMulTorsionFree.pow_eq_one_iff' := IsMulTorsionFree.pow_eq_one_iff_right
+alias IsMulTorsionFree.pow_eq_one_iff' := 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_left (by lia)
+lemma sq_eq_one : a ^ 2 = 1 ↔ a = 1 := pow_eq_one_iff_left (by lia)
 
 end Monoid
 

Mathlib/Algebra/GroupWithZero/Torsion.lean

@@ -41,7 +41,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_left hn] at hxy
+    Units.val_eq_one, pow_eq_one_iff_left hn] at hxy
   rwa [hxy, Units.val_one, mul_one] at hu
 
 end UniqueFactorizationMonoid

Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

@@ -222,11 +222,6 @@ theorem one_lt_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 < x ^ n ↔ 1 < x :=
 theorem pow_lt_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n < 1 ↔ x < 1 :=
   lt_iff_lt_of_le_iff_le (one_le_pow_iff hn)
 
-@[to_additive]
-theorem pow_eq_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 := by
-  simp only [le_antisymm_iff]
-  rw [pow_le_one_iff hn, one_le_pow_iff hn]
-
 end CovariantLE
 
 section CovariantLT

Mathlib/Algebra/Order/Ring/Basic.lean

@@ -35,20 +35,6 @@ lemma not_isSquare_of_neg [Semiring R] [LinearOrder R]
     {x : R} (h : x < 0) : ¬ IsSquare x :=
   (h.not_ge ·.nonneg)
 
-namespace MonoidHom
-
-variable [Ring R] [Monoid M] [LinearOrder M] [MulLeftMono M] (f : R →* M)
-
-theorem map_neg_one : f (-1) = 1 :=
-  (pow_eq_one_iff (Nat.succ_ne_zero 1)).1 <| by rw [← map_pow, neg_one_sq, map_one]
-
-@[simp]
-theorem map_neg (x : R) : f (-x) = f x := by rw [← neg_one_mul, map_mul, map_neg_one, one_mul]
-
-theorem map_sub_swap (x y : R) : f (x - y) = f (y - x) := by rw [← map_neg, neg_sub]
-
-end MonoidHom
-
 section OrderedSemiring
 
 variable [Semiring R] [PartialOrder R] [IsOrderedRing R] {a b x y : R} {n : ℕ}

Mathlib/Algebra/Ring/NonZeroDivisors.lean

@@ -30,8 +30,8 @@ theorem IsLeftRegular.pow_injective [IsMulTorsionFree R]
   intro n m hnm
   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_right hx'] at h₂
+    rw [pow_add, eq_comm, IsLeftRegular.mul_left_eq_self_iff (hx.pow n), 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

Mathlib/Algebra/Ring/Torsion.lean

@@ -6,7 +6,9 @@ Authors: Kim Morrison
 module
 
 public import Mathlib.Algebra.CharZero.Defs
+public import Mathlib.Algebra.Group.Torsion
 public import Mathlib.Algebra.GroupWithZero.Basic
+public import Mathlib.Algebra.Ring.Commute
 public import Mathlib.Algebra.Ring.Regular
 
 /-!
@@ -28,3 +30,15 @@ scoped instance (R : Type*) [Semiring R] [IsDomain R] [CharZero R] :
     grind
 
 end IsDomain
+
+namespace MonoidHom
+variable {R M : Type*} [Ring R] [Monoid M] [IsMulTorsionFree M] (f : R →* M)
+
+lemma map_neg_one : f (-1) = 1 :=
+  (pow_eq_one_iff_left (Nat.succ_ne_zero 1)).1 <| by rw [← map_pow, neg_one_sq, map_one]
+
+@[simp] lemma map_neg (x : R) : f (-x) = f x := by rw [← neg_one_mul, map_mul, map_neg_one, one_mul]
+
+lemma map_sub_swap (x y : R) : f (x - y) = f (y - x) := by rw [← map_neg, neg_sub]
+
+end MonoidHom

Mathlib/Data/Nat/Prime/Pow.lean

@@ -23,7 +23,7 @@ namespace Nat
 theorem pow_minFac {n k : ℕ} (hk : k ≠ 0) : (n ^ k).minFac = n.minFac := by
   rcases eq_or_ne n 1 with (rfl | hn)
   · simp
-  have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff hk).1 hk')
+  have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff_left hk).1 hk')
   apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm
   apply
     minFac_le_of_dvd (minFac_prime hnk).two_le

Mathlib/FieldTheory/Finite/GaloisField.lean

@@ -270,9 +270,7 @@ def ringEquivOfCardEq (hKK' : Fintype.card K = Fintype.card K') : K ≃+* K' :=
   choose n' hp' hK' using FiniteField.card K' p'
   have hpp' : p = p' := by
     by_contra hne
-    have h2 := Nat.coprime_pow_primes n n' hp hp' hne
-    rw [(Eq.congr hK hK').mp hKK', Nat.coprime_self, pow_eq_one_iff (PNat.ne_zero n')] at h2
-    exact Nat.Prime.ne_one hp' h2
+    simpa [← hK, hK', hKK', hp'.ne_one] using Nat.coprime_pow_primes n n' hp hp' hne
   rw [← hpp'] at _char_p'_K'
   haveI := fact_iff.2 hp
   letI : Algebra (ZMod p) K := ZMod.algebra _ _

Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean

@@ -161,11 +161,7 @@ theorem moebius_mul_coe_zeta : (μ * ζ : ArithmeticFunction ℤ) = 1 := by
   | one => simp
   | prime_pow p n hp hn =>
     rw [coe_mul_zeta_apply, sum_divisors_prime_pow hp, sum_range_succ']
-    simp_rw [pow_zero, moebius_apply_one, moebius_apply_prime_pow hp (succ_ne_zero _), succ_inj,
-      sum_ite_eq', mem_range, if_pos hn, neg_add_cancel]
-    rw [one_apply_ne]
-    rw [Ne, pow_eq_one_iff hn.ne']
-    exact hp.ne_one
+    simp [moebius_apply_prime_pow, hp.ne_one, hn.ne', hp, hn]
   | coprime a b _ha _hb hab ha' hb' =>
     rw [IsMultiplicative.map_mul_of_coprime _ hab, ha', hb',
       IsMultiplicative.map_mul_of_coprime isMultiplicative_one hab]

Mathlib/RingTheory/Valuation/Basic.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.GroupWithZero.Range
 public import Mathlib.Algebra.Order.Hom.Monoid
 public import Mathlib.Algebra.Order.Ring.Basic
+public import Mathlib.Algebra.Ring.Torsion
 public import Mathlib.RingTheory.Ideal.Maps
 public import Mathlib.Tactic.TFAE