From 9dc4b8ecd8695445ad7d717da17665ce617e1786 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 31 May 2022 20:07:51 +0000
Subject: [PATCH] =?UTF-8?q?feat(algebra/group=5Fpower/basic):=20`a^2=20=3D?=
 =?UTF-8?q?=20b^2=20=E2=86=94=20a=20=3D=20b=20=E2=88=A8=20a=20=3D=20-b`=20?=
 =?UTF-8?q?(#14431)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Generalize `a ^ 2 = 1 ↔ a = 1 ∨ a = -1` to `ring` + `no_zero_divisors` and prove `a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b` under `comm_ring` + `no_zero_divisors`.
---
 src/algebra/group_power/basic.lean            | 44 ++++++++++++-------
 src/algebra/group_power/order.lean            |  6 ---
 .../legendre_symbol/quadratic_char.lean       |  2 +-
 3 files changed, 30 insertions(+), 22 deletions(-)

diff --git a/src/algebra/group_power/basic.lean b/src/algebra/group_power/basic.lean
index 1794977b0a46f..a43c669224a57 100644
--- a/src/algebra/group_power/basic.lean
+++ b/src/algebra/group_power/basic.lean
@@ -399,7 +399,10 @@ alias neg_one_sq ← neg_one_pow_two
 end has_distrib_neg
 
 section ring
-variable [ring R]
+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 :=
@@ -409,21 +412,26 @@ by rcases neg_one_pow_eq_or R n; simp [h]
 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) :=
-by rw [sq, sq, mul_self_sub_mul_self]
+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 eq_or_eq_neg_of_sq_eq_sq [no_zero_divisors R] (a b : R) (h : a ^ 2 = b ^ 2) :
-  a = b ∨ a = -b :=
-by rwa [← add_eq_zero_iff_eq_neg, ← sub_eq_zero, or_comm, ← mul_eq_zero,
-        ← sq_sub_sq a b, sub_eq_zero]
-
 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]
 
@@ -432,16 +440,22 @@ 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
 
-lemma eq_or_eq_neg_of_sq_eq_sq [no_zero_divisors R] (a b : Rˣ) (h : a ^ 2 = b ^ 2) :
-  a = b ∨ a = -b :=
-begin
-  refine (eq_or_eq_neg_of_sq_eq_sq _ _ _).imp (λ h, units.ext h) (λ h, units.ext h),
-  replace h := congr_arg (coe : Rˣ → R) h,
-  rwa [units.coe_pow, units.coe_pow] at h,
-end
+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
 
diff --git a/src/algebra/group_power/order.lean b/src/algebra/group_power/order.lean
index d60b7e4d4b865..16518aa06aa0f 100644
--- a/src/algebra/group_power/order.lean
+++ b/src/algebra/group_power/order.lean
@@ -381,12 +381,6 @@ lemma sq_eq_sq_iff_abs_eq_abs (x y : R) : x^2 = y^2 ↔ |x| = |y| :=
 ⟨λ h, (abs_le_abs_of_sq_le_sq h.le).antisymm (abs_le_abs_of_sq_le_sq h.ge),
  λ h, by rw [←sq_abs, h, sq_abs]⟩
 
-@[simp] lemma sq_eq_one_iff (x : R) : x^2 = 1 ↔ x = 1 ∨ x = -1 :=
-by rw [←abs_eq_abs, ←sq_eq_sq_iff_abs_eq_abs, one_pow]
-
-lemma sq_ne_one_iff (x : R) : x^2 ≠ 1 ↔ x ≠ 1 ∧ x ≠ -1 :=
-(not_iff_not.2 (sq_eq_one_iff _)).trans not_or_distrib
-
 @[simp] lemma sq_le_one_iff_abs_le_one (x : R) : x^2 ≤ 1 ↔ |x| ≤ 1 :=
 have t : x^2 ≤ 1^2 ↔ |x| ≤ |1| := ⟨abs_le_abs_of_sq_le_sq, sq_le_sq⟩, by simpa using t
 
diff --git a/src/number_theory/legendre_symbol/quadratic_char.lean b/src/number_theory/legendre_symbol/quadratic_char.lean
index 5273b608d6874..00a942aed2b68 100644
--- a/src/number_theory/legendre_symbol/quadratic_char.lean
+++ b/src/number_theory/legendre_symbol/quadratic_char.lean
@@ -142,7 +142,7 @@ by rwa [pow_two, ← quadratic_char_mul, ← pow_two, quadratic_char_sq_one']
 /-- The quadratic character is `1` or `-1` on nonzero arguments. -/
 lemma quadratic_char_dichotomy {a : F} (ha : a ≠ 0) :
   quadratic_char F a = 1 ∨ quadratic_char F a = -1 :=
-(sq_eq_one_iff (quadratic_char F a)).mp (quadratic_char_sq_one ha)
+sq_eq_one_iff.1 $ quadratic_char_sq_one ha
 
 /-- A variant -/
 lemma quadratic_char_eq_neg_one_iff_not_one {a : F} (ha : a ≠ 0) :