feat(algebra/ring/basic): generalize lemmas about differences of squa…

…res to non-commutative rings (#12366)

This copies `mul_self_sub_mul_self` and `mul_self_eq_mul_self_iff` to the `commute` namespace, and reproves the existing lemmas in terms of the new commute lemmas.

As a result, the requirements on `mul_self_sub_one` and `mul_self_eq_one_iff` and `units.inv_eq_self_iff` can be weakened from `comm_ring` to `non_unital_non_assoc_ring` or `ring`.

This also replaces a few `is_domain`s with the weaker `no_zero_divisors`, since the lemmas are being moved anyway. In practice this just removes the nontriviality requirements.

src/algebra/ring/basic.lean

@@ -1075,13 +1075,6 @@ protected def function.surjective.comm_ring
 
 local attribute [simp] add_assoc add_comm add_left_comm mul_comm
 
-/-- Representation of a difference of two squares in a commutative ring as a product. -/
-theorem mul_self_sub_mul_self (a b : α) : a * a - b * b = (a + b) * (a - b) :=
-by rw [add_mul, mul_sub, mul_sub, mul_comm a b, sub_add_sub_cancel]
-
-lemma mul_self_sub_one (a : α) : a * a - 1 = (a + 1) * (a - 1) :=
-by rw [← mul_self_sub_mul_self, mul_one]
-
 /-- Vieta's formula for a quadratic equation, relating the coefficients of the polynomial with
   its roots. This particular version states that if we have a root `x` of a monic quadratic
   polynomial, then there is another root `y` such that `x + y` is negative the `a_1` coefficient
@@ -1186,18 +1179,6 @@ variables [comm_ring α] [is_domain α]
 instance is_domain.to_cancel_comm_monoid_with_zero : cancel_comm_monoid_with_zero α :=
 { ..comm_semiring.to_comm_monoid_with_zero, ..is_domain.to_cancel_monoid_with_zero }
 
-lemma mul_self_eq_mul_self_iff {a b : α} : a * a = b * b ↔ a = b ∨ a = -b :=
-by rw [← sub_eq_zero, mul_self_sub_mul_self, mul_eq_zero, or_comm, sub_eq_zero,
-  add_eq_zero_iff_eq_neg]
-
-lemma mul_self_eq_one_iff {a : α} : a * a = 1 ↔ a = 1 ∨ a = -1 :=
-by rw [← mul_self_eq_mul_self_iff, one_mul]
-
-/-- In the unit group of an integral domain, a unit is its own inverse iff the unit is one or
-  one's additive inverse. -/
-lemma units.inv_eq_self_iff (u : αˣ) : u⁻¹ = u ↔ u = 1 ∨ u = -1 :=
-by { rw inv_eq_iff_mul_eq_one, simp only [units.ext_iff], push_cast, exact mul_self_eq_one_iff }
-
 /--
 Makes a ring homomorphism from an additive group homomorphism from a commutative ring to an integral
 domain that commutes with self multiplication, assumes that two is nonzero and one is sent to one.
@@ -1309,6 +1290,20 @@ h.bit0_right.add_right (commute.one_right x)
 lemma bit1_left [semiring R] {x y : R} (h : commute x y) : commute (bit1 x) y :=
 h.bit0_left.add_left (commute.one_left y)
 
+/-- Representation of a difference of two squares of commuting elements as a product. -/
+lemma mul_self_sub_mul_self_eq [non_unital_non_assoc_ring R] {a b : R} (h : commute a b) :
+  a * a - b * b = (a + b) * (a - b) :=
+by rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]
+
+lemma mul_self_sub_mul_self_eq' [non_unital_non_assoc_ring R] {a b : R} (h : commute a b) :
+  a * a - b * b = (a - b) * (a + b) :=
+by rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]
+
+lemma mul_self_eq_mul_self_iff [non_unital_non_assoc_ring R] [no_zero_divisors R] {a b : R}
+  (h : commute a b) : a * a = b * b ↔ a = b ∨ a = -b :=
+by rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
+  add_eq_zero_iff_eq_neg]
+
 section
 variables [has_mul R] [has_distrib_neg R] {a b : R}
 
@@ -1337,3 +1332,28 @@ variables [ring R] {a b c : R}
 end
 
 end commute
+
+/-- Representation of a difference of two squares in a commutative ring as a product. -/
+theorem mul_self_sub_mul_self [comm_ring R] (a b : R) : a * a - b * b = (a + b) * (a - b) :=
+(commute.all a b).mul_self_sub_mul_self_eq
+
+lemma mul_self_sub_one [non_assoc_ring R] (a : R) : a * a - 1 = (a + 1) * (a - 1) :=
+by rw [←(commute.one_right a).mul_self_sub_mul_self_eq, mul_one]
+
+lemma mul_self_eq_mul_self_iff [comm_ring R] [no_zero_divisors R] {a b : R} :
+  a * a = b * b ↔ a = b ∨ a = -b :=
+(commute.all a b).mul_self_eq_mul_self_iff
+
+lemma mul_self_eq_one_iff [non_assoc_ring R] [no_zero_divisors R] {a : R} :
+  a * a = 1 ↔ a = 1 ∨ a = -1 :=
+by rw [←(commute.one_right a).mul_self_eq_mul_self_iff, mul_one]
+
+/-- In the unit group of an integral domain, a unit is its own inverse iff the unit is one or
+  one's additive inverse. -/
+lemma units.inv_eq_self_iff [ring R] [no_zero_divisors R] (u : Rˣ) : u⁻¹ = u ↔ u = 1 ∨ u = -1 :=
+begin
+  rw inv_eq_iff_mul_eq_one,
+  simp only [units.ext_iff],
+  push_cast,
+  exact mul_self_eq_one_iff
+end