chore: Move ring power lemmas earlier

After #12817, almost all lemmas can move from `Algebra.GroupPower.Ring` to earlier files at no cost.

The few remaining lemmas could also move, but it would require a tiny bit more work.

Mathlib/Algebra/GroupPower/Ring.lean

@@ -3,10 +3,9 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
-import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Divisibility
-import Mathlib.Algebra.Ring.Commute
-import Mathlib.Algebra.Ring.Divisibility.Basic
+import Mathlib.Algebra.GroupWithZero.Hom
+import Mathlib.Algebra.Ring.Defs
 
 #align_import algebra.group_power.ring from "leanprover-community/mathlib"@"fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e"
 
@@ -19,19 +18,6 @@ Further lemmas about ordered semirings and rings can be found in `Algebra.GroupP
 
 variable {R S M : Type*}
 
-section MonoidWithZero
-
-variable [MonoidWithZero M]
-
-theorem Ring.inverse_pow (r : M) : ∀ n : ℕ, Ring.inverse r ^ n = Ring.inverse (r ^ n)
-  | 0 => by rw [pow_zero, pow_zero, Ring.inverse_one]
-  | n + 1 => by
-    rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
-      Ring.inverse_pow r n]
-#align ring.inverse_pow Ring.inverse_pow
-
-end MonoidWithZero
-
 section CommMonoidWithZero
 
 variable [CommMonoidWithZero M] {n : ℕ} (hn : n ≠ 0)
@@ -67,90 +53,6 @@ theorem pow_dvd_pow_iff [CancelCommMonoidWithZero R] {x : R} {n m : ℕ} (h0 : x
   · apply pow_dvd_pow
 #align pow_dvd_pow_iff pow_dvd_pow_iff
 
-section Semiring
-
-variable [Semiring R] [Semiring S]
-
-protected theorem RingHom.map_pow (f : R →+* S) (a) : ∀ n : ℕ, f (a ^ n) = f a ^ n :=
-  map_pow f a
-#align ring_hom.map_pow RingHom.map_pow
-
-theorem min_pow_dvd_add {n m : ℕ} {a b c : R} (ha : c ^ n ∣ a) (hb : c ^ m ∣ b) :
-    c ^ min n m ∣ a + b := by
-  replace ha := (pow_dvd_pow c (min_le_left n m)).trans ha
-  replace hb := (pow_dvd_pow c (min_le_right n m)).trans hb
-  exact dvd_add ha hb
-#align min_pow_dvd_add min_pow_dvd_add
-
-end Semiring
-
-section CommSemiring
-
-variable [CommSemiring R]
-
-theorem add_sq (a b : R) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
-  simp only [sq, add_mul_self_eq]
-#align add_sq add_sq
-
-theorem add_sq' (a b : R) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b := by
-  rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]
-#align add_sq' add_sq'
-
-alias add_pow_two := add_sq
-#align add_pow_two add_pow_two
-
-end CommSemiring
-
-section HasDistribNeg
-
-variable [Monoid R] [HasDistribNeg R]
-variable (R)
-
-theorem neg_one_pow_eq_or : ∀ n : ℕ, (-1 : R) ^ n = 1 ∨ (-1 : R) ^ n = -1
-  | 0 => Or.inl (pow_zero _)
-  | n + 1 => (neg_one_pow_eq_or n).symm.imp
-    (fun h ↦ by rw [pow_succ, h, neg_one_mul, neg_neg])
-    (fun h ↦ by rw [pow_succ, h, one_mul])
-#align neg_one_pow_eq_or neg_one_pow_eq_or
-
-variable {R}
-
-theorem neg_pow (a : R) (n : ℕ) : (-a) ^ n = (-1) ^ n * a ^ n :=
-  neg_one_mul a ▸ (Commute.neg_one_left a).mul_pow n
-#align neg_pow neg_pow
-
-theorem neg_pow' (a : R) (n : ℕ) : (-a) ^ n = a ^ n * (-1) ^ n :=
-  mul_neg_one a ▸ (Commute.neg_one_right a).mul_pow n
-
-section
-set_option linter.deprecated false
-
-theorem neg_pow_bit0 (a : R) (n : ℕ) : (-a) ^ bit0 n = a ^ bit0 n := by
-  rw [pow_bit0', neg_mul_neg, pow_bit0']
-#align neg_pow_bit0 neg_pow_bit0
-
-@[simp]
-theorem neg_pow_bit1 (a : R) (n : ℕ) : (-a) ^ bit1 n = -a ^ bit1 n := by
-  simp only [bit1, pow_succ', neg_pow_bit0, neg_mul_eq_neg_mul]
-#align neg_pow_bit1 neg_pow_bit1
-
-end
-
-theorem neg_sq (a : R) : (-a) ^ 2 = a ^ 2 := by simp [sq]
-#align neg_sq neg_sq
-
--- Porting note: removed the simp attribute to please the simpNF linter
-theorem neg_one_sq : (-1 : R) ^ 2 = 1 := by simp [neg_sq, one_pow]
-#align neg_one_sq neg_one_sq
-
-alias neg_pow_two := neg_sq
-#align neg_pow_two neg_pow_two
-
-alias neg_one_pow_two := neg_one_sq
-#align neg_one_pow_two neg_one_pow_two
-
-end HasDistribNeg
-
 section DivisionMonoid
 variable [DivisionMonoid R] [HasDistribNeg R]
 
@@ -160,90 +62,3 @@ set_option linter.deprecated false in
 #align zpow_bit0_neg zpow_bit0_neg
 
 end DivisionMonoid
-
-section Ring
-
-variable [Ring R] {a b : R}
-
-protected theorem Commute.sq_sub_sq (h : Commute a b) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := by
-  rw [sq, sq, h.mul_self_sub_mul_self_eq]
-#align commute.sq_sub_sq Commute.sq_sub_sq
-
-@[simp]
-theorem neg_one_pow_mul_eq_zero_iff {n : ℕ} {r : R} : (-1) ^ n * r = 0 ↔ r = 0 := by
-  rcases neg_one_pow_eq_or R n with h | h <;> simp [h]
-#align neg_one_pow_mul_eq_zero_iff neg_one_pow_mul_eq_zero_iff
-
-@[simp]
-theorem mul_neg_one_pow_eq_zero_iff {n : ℕ} {r : R} : r * (-1) ^ n = 0 ↔ r = 0 := by
-  rcases neg_one_pow_eq_or R n with h | h <;> simp [h]
-#align mul_neg_one_pow_eq_zero_iff mul_neg_one_pow_eq_zero_iff
-
-variable [NoZeroDivisors R]
-
-protected theorem Commute.sq_eq_sq_iff_eq_or_eq_neg (h : Commute a b) :
-    a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b := by
-  rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]
-#align commute.sq_eq_sq_iff_eq_or_eq_neg Commute.sq_eq_sq_iff_eq_or_eq_neg
-
-@[simp]
-theorem sq_eq_one_iff : a ^ 2 = 1 ↔ a = 1 ∨ a = -1 := by
-  rw [← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg, one_pow]
-#align sq_eq_one_iff sq_eq_one_iff
-
-theorem sq_ne_one_iff : a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1 :=
-  sq_eq_one_iff.not.trans not_or
-#align sq_ne_one_iff sq_ne_one_iff
-
-lemma neg_one_pow_eq_pow_mod_two (n : ℕ) : (-1 : R) ^ n = (-1) ^ (n % 2) := by
-  rw [← Nat.mod_add_div n 2, pow_add, pow_mul]; simp [sq]
-#align neg_one_pow_eq_pow_mod_two neg_one_pow_eq_pow_mod_two
-
-end Ring
-
-section CommRing
-
-variable [CommRing R]
-
-theorem sq_sub_sq (a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b) :=
-  (Commute.all a b).sq_sub_sq
-#align sq_sub_sq sq_sub_sq
-
-alias pow_two_sub_pow_two := sq_sub_sq
-#align pow_two_sub_pow_two pow_two_sub_pow_two
-
-theorem sub_sq (a b : R) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2 := by
-  rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
-#align sub_sq sub_sq
-
-alias sub_pow_two := sub_sq
-#align sub_pow_two sub_pow_two
-
-theorem sub_sq' (a b : R) : (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b := by
-  rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]
-#align sub_sq' sub_sq'
-
-variable [NoZeroDivisors R] {a b : R}
-
-theorem sq_eq_sq_iff_eq_or_eq_neg : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b :=
-  (Commute.all a b).sq_eq_sq_iff_eq_or_eq_neg
-#align sq_eq_sq_iff_eq_or_eq_neg sq_eq_sq_iff_eq_or_eq_neg
-
-theorem eq_or_eq_neg_of_sq_eq_sq (a b : R) : a ^ 2 = b ^ 2 → a = b ∨ a = -b :=
-  sq_eq_sq_iff_eq_or_eq_neg.1
-#align eq_or_eq_neg_of_sq_eq_sq eq_or_eq_neg_of_sq_eq_sq
-
--- Copies of the above CommRing lemmas for `Units R`.
-namespace Units
-
-protected theorem sq_eq_sq_iff_eq_or_eq_neg {a b : Rˣ} : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b := by
-  simp_rw [ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]
-#align units.sq_eq_sq_iff_eq_or_eq_neg Units.sq_eq_sq_iff_eq_or_eq_neg
-
-protected theorem eq_or_eq_neg_of_sq_eq_sq (a b : Rˣ) (h : a ^ 2 = b ^ 2) : a = b ∨ a = -b :=
-  Units.sq_eq_sq_iff_eq_or_eq_neg.1 h
-#align units.eq_or_eq_neg_of_sq_eq_sq Units.eq_or_eq_neg_of_sq_eq_sq
-
-end Units
-
-end CommRing

Mathlib/Algebra/GroupWithZero/Commute.lean

@@ -37,6 +37,13 @@ theorem mul_inverse_rev {M₀} [CommMonoidWithZero M₀] (a b : M₀) :
   mul_inverse_rev' (Commute.all _ _)
 #align ring.mul_inverse_rev Ring.mul_inverse_rev
 
+lemma inverse_pow (r : M₀) : ∀ n : ℕ, Ring.inverse r ^ n = Ring.inverse (r ^ n)
+  | 0 => by rw [pow_zero, pow_zero, Ring.inverse_one]
+  | n + 1 => by
+    rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
+      Ring.inverse_pow r n]
+#align ring.inverse_pow Ring.inverse_pow
+
 end Ring
 
 theorem Commute.ring_inverse_ring_inverse {a b : M₀} (h : Commute a b) :

Mathlib/Algebra/Ring/Commute.lean

@@ -143,8 +143,97 @@ theorem sub_left : Commute a c → Commute b c → Commute (a - b) c :=
 
 end
 
+section Ring
+variable [Ring R] {a b : R}
+
+protected lemma sq_sub_sq (h : Commute a b) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := by
+  rw [sq, sq, h.mul_self_sub_mul_self_eq]
+#align commute.sq_sub_sq Commute.sq_sub_sq
+
+variable [NoZeroDivisors R]
+
+protected lemma sq_eq_sq_iff_eq_or_eq_neg (h : Commute a b) : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b := by
+  rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]
+#align commute.sq_eq_sq_iff_eq_or_eq_neg Commute.sq_eq_sq_iff_eq_or_eq_neg
+
+end Ring
 end Commute
 
+section HasDistribNeg
+variable (R)
+variable [Monoid R] [HasDistribNeg R]
+
+lemma neg_one_pow_eq_or : ∀ n : ℕ, (-1 : R) ^ n = 1 ∨ (-1 : R) ^ n = -1
+  | 0 => Or.inl (pow_zero _)
+  | n + 1 => (neg_one_pow_eq_or n).symm.imp
+    (fun h ↦ by rw [pow_succ, h, neg_one_mul, neg_neg])
+    (fun h ↦ by rw [pow_succ, h, one_mul])
+#align neg_one_pow_eq_or neg_one_pow_eq_or
+
+variable {R}
+
+lemma neg_pow (a : R) (n : ℕ) : (-a) ^ n = (-1) ^ n * a ^ n :=
+  neg_one_mul a ▸ (Commute.neg_one_left a).mul_pow n
+#align neg_pow neg_pow
+
+lemma neg_pow' (a : R) (n : ℕ) : (-a) ^ n = a ^ n * (-1) ^ n :=
+  mul_neg_one a ▸ (Commute.neg_one_right a).mul_pow n
+
+section
+set_option linter.deprecated false
+
+lemma neg_pow_bit0 (a : R) (n : ℕ) : (-a) ^ bit0 n = a ^ bit0 n := by
+  rw [pow_bit0', neg_mul_neg, pow_bit0']
+#align neg_pow_bit0 neg_pow_bit0
+
+@[simp]
+lemma neg_pow_bit1 (a : R) (n : ℕ) : (-a) ^ bit1 n = -a ^ bit1 n := by
+  simp only [bit1, pow_succ', neg_pow_bit0, neg_mul_eq_neg_mul]
+#align neg_pow_bit1 neg_pow_bit1
+
+end
+
+lemma neg_sq (a : R) : (-a) ^ 2 = a ^ 2 := by simp [sq]
+#align neg_sq neg_sq
+
+-- Porting note: removed the simp attribute to please the simpNF linter
+lemma neg_one_sq : (-1 : R) ^ 2 = 1 := by simp [neg_sq, one_pow]
+#align neg_one_sq neg_one_sq
+
+alias neg_pow_two := neg_sq
+#align neg_pow_two neg_pow_two
+
+alias neg_one_pow_two := neg_one_sq
+#align neg_one_pow_two neg_one_pow_two
+
+end HasDistribNeg
+
+section Ring
+variable [Ring R] {a b : R} {n : ℕ}
+
+@[simp] lemma neg_one_pow_mul_eq_zero_iff : (-1) ^ n * a = 0 ↔ a = 0 := by
+  rcases neg_one_pow_eq_or R n with h | h <;> simp [h]
+#align neg_one_pow_mul_eq_zero_iff neg_one_pow_mul_eq_zero_iff
+
+@[simp] lemma mul_neg_one_pow_eq_zero_iff : a * (-1) ^ n = 0 ↔ a = 0 := by
+  obtain h | h := neg_one_pow_eq_or R n <;> simp [h]
+#align mul_neg_one_pow_eq_zero_iff mul_neg_one_pow_eq_zero_iff
+
+variable [NoZeroDivisors R]
+
+@[simp] lemma sq_eq_one_iff : a ^ 2 = 1 ↔ a = 1 ∨ a = -1 := by
+  rw [← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg, one_pow]
+#align sq_eq_one_iff sq_eq_one_iff
+
+lemma sq_ne_one_iff : a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1 := sq_eq_one_iff.not.trans not_or
+#align sq_ne_one_iff sq_ne_one_iff
+
+lemma neg_one_pow_eq_pow_mod_two (n : ℕ) : (-1 : R) ^ n = (-1) ^ (n % 2) := by
+  rw [← Nat.mod_add_div n 2, pow_add, pow_mul]; simp [sq]
+#align neg_one_pow_eq_pow_mod_two neg_one_pow_eq_pow_mod_two
+
+end Ring
+
 /-- Representation of a difference of two squares in a commutative ring as a product. -/
 theorem mul_self_sub_mul_self [CommRing R] (a b : R) : a * a - b * b = (a + b) * (a - b) :=
   (Commute.all a b).mul_self_sub_mul_self_eq
@@ -164,6 +253,50 @@ theorem mul_self_eq_one_iff [NonAssocRing R] [NoZeroDivisors R] {a : R} :
   rw [← (Commute.one_right a).mul_self_eq_mul_self_iff, mul_one]
 #align mul_self_eq_one_iff mul_self_eq_one_iff
 
+section CommRing
+variable [CommRing R]
+
+lemma sq_sub_sq (a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := (Commute.all a b).sq_sub_sq
+#align sq_sub_sq sq_sub_sq
+
+alias pow_two_sub_pow_two := sq_sub_sq
+#align pow_two_sub_pow_two pow_two_sub_pow_two
+
+lemma sub_sq (a b : R) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2 := by
+  rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
+#align sub_sq sub_sq
+
+alias sub_pow_two := sub_sq
+#align sub_pow_two sub_pow_two
+
+lemma sub_sq' (a b : R) : (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b := by
+  rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]
+#align sub_sq' sub_sq'
+
+variable [NoZeroDivisors R] {a b : R}
+
+lemma sq_eq_sq_iff_eq_or_eq_neg : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b :=
+  (Commute.all a b).sq_eq_sq_iff_eq_or_eq_neg
+#align sq_eq_sq_iff_eq_or_eq_neg sq_eq_sq_iff_eq_or_eq_neg
+
+lemma eq_or_eq_neg_of_sq_eq_sq (a b : R) : a ^ 2 = b ^ 2 → a = b ∨ a = -b :=
+  sq_eq_sq_iff_eq_or_eq_neg.1
+#align eq_or_eq_neg_of_sq_eq_sq eq_or_eq_neg_of_sq_eq_sq
+
+-- Copies of the above CommRing lemmas for `Units R`.
+namespace Units
+
+protected lemma sq_eq_sq_iff_eq_or_eq_neg {a b : Rˣ} : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b := by
+  simp_rw [ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]
+#align units.sq_eq_sq_iff_eq_or_eq_neg Units.sq_eq_sq_iff_eq_or_eq_neg
+
+protected lemma eq_or_eq_neg_of_sq_eq_sq (a b : Rˣ) (h : a ^ 2 = b ^ 2) : a = b ∨ a = -b :=
+  Units.sq_eq_sq_iff_eq_or_eq_neg.1 h
+#align units.eq_or_eq_neg_of_sq_eq_sq Units.eq_or_eq_neg_of_sq_eq_sq
+
+end Units
+end CommRing
+
 namespace Units
 
 /-- In the unit group of an integral domain, a unit is its own inverse iff the unit is one or

Mathlib/Algebra/Ring/Defs.lean

@@ -284,6 +284,17 @@ theorem add_mul_self_eq (a b : α) : (a + b) * (a + b) = a * a + 2 * a * b + b *
   simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]
 #align add_mul_self_eq add_mul_self_eq
 
+lemma add_sq (a b : α) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
+  simp only [sq, add_mul_self_eq]
+#align add_sq add_sq
+
+lemma add_sq' (a b : α) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b := by
+  rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]
+#align add_sq' add_sq'
+
+alias add_pow_two := add_sq
+#align add_pow_two add_pow_two
+
 end CommSemiring
 
 section HasDistribNeg