refactor(algebra/group_power): split ring lemmas into a separate file (#15032)

This doesn't actually stop `algebra.ring.basic` being imported into `group_power.basic` yet, but it makes it easier to make that change in future. Two ~300 line files are also slightly easier to manage than one ~600 line file, and ring/add_group feels like a natural place to draw the line

All lemmas have just been moved, and none have been renamed. Some lemmas have had their `R` variables renamed to `M` to better reflect that they apply to monoids with zero.

By grouping together the `monoid_with_zero` lemmas from separate files, it become apparent that there's some overlap.
This PR does not attempt to clean this up, in the interest of limiting the the scope of this change to just moves.

Author: eric-wieser

src/algebra/group_power/basic.lean

@@ -3,7 +3,8 @@ 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 algebra.hom.ring
+import algebra.divisibility
+import algebra.group.commute
 import data.nat.basic
 
 /-!
@@ -281,219 +282,13 @@ by rw [pow_sub a⁻¹ h, inv_pow, inv_pow, inv_inv]
 
 end group
 
-lemma zero_pow [monoid_with_zero R] : ∀ {n : ℕ}, 0 < n → (0 : R) ^ n = 0
-| (n+1) _ := by rw [pow_succ, zero_mul]
-
-lemma zero_pow_eq [monoid_with_zero R] (n : ℕ) : (0 : R)^n = if n = 0 then 1 else 0 :=
-begin
-  split_ifs with h,
-  { rw [h, pow_zero], },
-  { rw [zero_pow (nat.pos_of_ne_zero h)] },
-end
-
-lemma pow_eq_zero_of_le [monoid_with_zero M] {x : M} {n m : ℕ}
-  (hn : n ≤ m) (hx : x^n = 0) : x^m = 0 :=
-by rw [← tsub_add_cancel_of_le hn, pow_add, hx, mul_zero]
-
-namespace ring_hom
-
-variables [semiring R] [semiring S]
-
-protected lemma map_pow (f : R →+* S) (a) :
-  ∀ n : ℕ, f (a ^ n) = (f a) ^ n :=
-map_pow f a
-
-end ring_hom
-
-section pow_monoid_with_zero_hom
-
-variables [comm_monoid_with_zero M] {n : ℕ} (hn : 0 < n)
-include M hn
-
-/-- We define `x ↦ x^n` (for positive `n : ℕ`) as a `monoid_with_zero_hom` -/
-def pow_monoid_with_zero_hom : M →*₀ M :=
-{ map_zero' := zero_pow hn,
-  ..pow_monoid_hom n }
-
-@[simp]
-lemma coe_pow_monoid_with_zero_hom : (pow_monoid_with_zero_hom hn : M → M) = (^ n) := rfl
-
-@[simp]
-lemma pow_monoid_with_zero_hom_apply (a : M) : pow_monoid_with_zero_hom hn a = a ^ n := rfl
-
-end pow_monoid_with_zero_hom
-
 lemma pow_dvd_pow [monoid R] (a : R) {m n : ℕ} (h : m ≤ n) :
   a ^ m ∣ a ^ n := ⟨a ^ (n - m), by rw [← pow_add, nat.add_comm, tsub_add_cancel_of_le h]⟩
 
 theorem pow_dvd_pow_of_dvd [comm_monoid R] {a b : R} (h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n
 | 0     := by rw [pow_zero, pow_zero]
 | (n+1) := by { rw [pow_succ, pow_succ], exact mul_dvd_mul h (pow_dvd_pow_of_dvd n) }
 
-theorem pow_eq_zero [monoid_with_zero R] [no_zero_divisors R] {x : R} {n : ℕ} (H : x^n = 0) :
-  x = 0 :=
-begin
-  induction n with n ih,
-  { rw pow_zero at H,
-    rw [← mul_one x, H, mul_zero] },
-  { rw pow_succ at H,
-    exact or.cases_on (mul_eq_zero.1 H) id ih }
-end
-
-@[simp] lemma pow_eq_zero_iff [monoid_with_zero R] [no_zero_divisors R]
-  {a : R} {n : ℕ} (hn : 0 < n) :
-  a ^ n = 0 ↔ a = 0 :=
-begin
-  refine ⟨pow_eq_zero, _⟩,
-  rintros rfl,
-  exact zero_pow hn,
-end
-
-lemma pow_eq_zero_iff' [monoid_with_zero R] [no_zero_divisors R] [nontrivial R]
-  {a : R} {n : ℕ} :
-  a ^ n = 0 ↔ a = 0 ∧ n ≠ 0 :=
-by cases (zero_le n).eq_or_gt; simp [*, ne_of_gt]
-
-lemma pow_ne_zero_iff [monoid_with_zero R] [no_zero_divisors R] {a : R} {n : ℕ} (hn : 0 < n) :
-  a ^ n ≠ 0 ↔ a ≠ 0 :=
-(pow_eq_zero_iff hn).not
-
-@[field_simps] theorem pow_ne_zero [monoid_with_zero R] [no_zero_divisors R]
-  {a : R} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
-mt pow_eq_zero h
-
-theorem sq_eq_zero_iff [monoid_with_zero R] [no_zero_divisors R] {a : R} : a ^ 2 = 0 ↔ a = 0 :=
-pow_eq_zero_iff two_pos
-
-lemma pow_dvd_pow_iff [cancel_comm_monoid_with_zero R]
-  {x : R} {n m : ℕ} (h0 : x ≠ 0) (h1 : ¬ is_unit x) :
-  x ^ n ∣ x ^ m ↔ n ≤ m :=
-begin
-  split,
-  { intro h, rw [← not_lt], intro hmn, apply h1,
-    have : x ^ m * x ∣ x ^ m * 1,
-    { rw [← pow_succ', mul_one], exact (pow_dvd_pow _ (nat.succ_le_of_lt hmn)).trans h },
-    rwa [mul_dvd_mul_iff_left, ← is_unit_iff_dvd_one] at this, apply pow_ne_zero m h0 },
-  { apply pow_dvd_pow }
-end
-
-section semiring
-variables [semiring R]
-
-lemma min_pow_dvd_add {n m : ℕ} {a b c : R} (ha : c ^ n ∣ a) (hb : c ^ m ∣ b) :
-  c ^ (min n m) ∣ a + b :=
-begin
-  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
-end
-
-end semiring
-
-section comm_semiring
-variables [comm_semiring R]
-
-lemma add_sq (a b : R) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 :=
-by simp only [sq, add_mul_self_eq]
-
-lemma 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]
-
-alias add_sq ← add_pow_two
-
-end comm_semiring
-
-section has_distrib_neg
-variables [monoid R] [has_distrib_neg R]
-
-variables (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).swap.imp
-  (λ h, by rw [pow_succ, h, neg_one_mul, neg_neg])
-  (λ h, by rw [pow_succ, h, mul_one])
-variables {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
-
-@[simp] theorem neg_pow_bit0 (a : R) (n : ℕ) : (- a) ^ (bit0 n) = a ^ (bit0 n) :=
-by rw [pow_bit0', neg_mul_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]
-
-@[simp] lemma neg_sq (a : R) : (-a) ^ 2 = a ^ 2 := by simp [sq]
-@[simp] lemma neg_one_sq : (-1 : R) ^ 2 = 1 := by rw [neg_sq, one_pow]
-
-alias neg_sq ← neg_pow_two
-alias neg_one_sq ← neg_one_pow_two
-
-end has_distrib_neg
-
-section ring
-variables [ring R] {a b : R}
-
-protected lemma 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]
-
-@[simp]
-lemma 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; simp [h]
-
-@[simp]
-lemma 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; simp [h]
-
-variables [no_zero_divisors R]
-
-protected lemma 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]
-
-@[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]
-
-lemma sq_ne_one_iff : a^2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1 := sq_eq_one_iff.not.trans not_or_distrib
-
-end ring
-
-section comm_ring
-variables [comm_ring R]
-
-lemma sq_sub_sq (a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := (commute.all a b).sq_sub_sq
-
-alias sq_sub_sq ← 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]
-
-alias sub_sq ← 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]
-
-variables [no_zero_divisors 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
-
-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
-
-/- Copies of the above comm_ring 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, coe_pow, sq_eq_sq_iff_eq_or_eq_neg, units.coe_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
-
-end units
-
-end comm_ring
-
 lemma of_add_nsmul [add_monoid A] (x : A) (n : ℕ) :
   multiplicative.of_add (n • x) = (multiplicative.of_add x)^n := rfl
 

src/algebra/group_power/lemmas.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import algebra.invertible
+import algebra.group_power.ring
 import data.int.cast
 
 /-!

src/algebra/group_power/order.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import algebra.order.ring
-import algebra.group_power.basic
+import algebra.group_power.ring
 
 /-!
 # Lemmas about the interaction of power operations with order