From 93a37647e9596744e08cf99f93ae5e6be84f0d85 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Sat, 17 Jul 2021 11:26:47 +0000
Subject: [PATCH] chore(algebra/ring/basic): drop commutativity assumptions
 from some division lemmas (#8334)

* Removes `dvd_neg_iff_dvd`, `neg_dvd_iff_dvd` which duplicated `dvd_neg`, `neg_dvd`.
* Generalizes `two_dvd_bit0` to non-commutative semirings.
* Generalizes a bunch of lemmas from `comm_ring` to `ring`.
* Adds `even_neg` for `ring` to replace `int.even_neg`.
---
 src/algebra/ring/basic.lean | 122 +++++++++++++++++++-----------------
 src/data/int/basic.lean     |   4 +-
 src/data/int/parity.lean    |   3 -
 3 files changed, 66 insertions(+), 63 deletions(-)

diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean
index 6cc9980f88a84..7010b80d77a5e 100644
--- a/src/algebra/ring/basic.lean
+++ b/src/algebra/ring/basic.lean
@@ -520,6 +520,14 @@ omit rα rβ rγ
 
 end ring_hom
 
+section semiring
+
+variables [semiring α] {a : α}
+
+@[simp] theorem two_dvd_bit0 : 2 ∣ bit0 a := ⟨a, bit0_eq_two_mul _⟩
+
+end semiring
+
 /-- A commutative semiring is a `semiring` with commutative multiplication. In other words, it is a
 type with the following structures: additive commutative monoid (`add_comm_monoid`), multiplicative
 commutative monoid (`comm_monoid`), distributive laws (`distrib`), and multiplication by zero law
@@ -555,8 +563,6 @@ protected def function.surjective.comm_semiring [has_zero γ] [has_one γ] [has_
 lemma add_mul_self_eq (a b : α) : (a + b) * (a + b) = a*a + 2*a*b + b*b :=
 by simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]
 
-@[simp] theorem two_dvd_bit0 : 2 ∣ bit0 a := ⟨a, bit0_eq_two_mul _⟩
-
 lemma ring_hom.map_dvd (f : α →+* β) {a b : α} : a ∣ b → f a ∣ f b :=
 λ ⟨z, hz⟩, ⟨f z, by rw [hz, f.map_mul]⟩
 
@@ -744,32 +750,8 @@ class comm_ring (α : Type u) extends ring α, comm_monoid α
 instance comm_ring.to_comm_semiring [s : comm_ring α] : comm_semiring α :=
 { mul_zero := mul_zero, zero_mul := zero_mul, ..s }
 
-section comm_ring
-variables [comm_ring α] {a b c : α}
-
-/-- Pullback a `comm_ring` instance along an injective function.
-See note [reducible non-instances]. -/
-@[reducible]
-protected def function.injective.comm_ring
-  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
-  (f : β → α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
-  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
-  (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) :
-  comm_ring β :=
-{ .. hf.ring f zero one add mul neg sub, .. hf.comm_semigroup f mul }
-
-/-- Pullback a `comm_ring` instance along an injective function.
-See note [reducible non-instances]. -/
-@[reducible]
-protected def function.surjective.comm_ring
-  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
-  (f : α → β) (hf : surjective f) (zero : f 0 = 0) (one : f 1 = 1)
-  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
-  (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) :
-  comm_ring β :=
-{ .. hf.ring f zero one add mul neg sub, .. hf.comm_semigroup f mul }
-
-local attribute [simp] add_assoc add_comm add_left_comm mul_comm
+section ring
+variables [ring α] {a b c : α}
 
 theorem dvd_neg_of_dvd (h : a ∣ b) : (a ∣ -b) :=
 dvd.elim h
@@ -779,7 +761,8 @@ dvd.elim h
 theorem dvd_of_dvd_neg (h : a ∣ -b) : (a ∣ b) :=
 let t := dvd_neg_of_dvd h in by rwa neg_neg at t
 
-theorem dvd_neg_iff_dvd (a b : α) : (a ∣ -b) ↔ (a ∣ b) :=
+/-- An element a of a ring divides the additive inverse of an element b iff a divides b. -/
+@[simp] lemma dvd_neg (a b : α) : (a ∣ -b) ↔ (a ∣ b) :=
 ⟨dvd_of_dvd_neg, dvd_neg_of_dvd⟩
 
 theorem neg_dvd_of_dvd (h : a ∣ b) : -a ∣ b :=
@@ -790,7 +773,8 @@ dvd.elim h
 theorem dvd_of_neg_dvd (h : -a ∣ b) : a ∣ b :=
 let t := neg_dvd_of_dvd h in by rwa neg_neg at t
 
-theorem neg_dvd_iff_dvd (a b : α) : (-a ∣ b) ↔ (a ∣ b) :=
+/-- The additive inverse of an element a of a ring divides another element b iff a divides b. -/
+@[simp] lemma neg_dvd (a b : α) : (-a ∣ b) ↔ (a ∣ b) :=
 ⟨dvd_of_neg_dvd, neg_dvd_of_dvd⟩
 
 theorem dvd_sub (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b - c :=
@@ -804,23 +788,6 @@ by rw add_comm; exact dvd_add_iff_left h
 
 theorem two_dvd_bit1 : 2 ∣ bit1 a ↔ (2 : α) ∣ 1 := (dvd_add_iff_right (@two_dvd_bit0 _ _ a)).symm
 
-/-- 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]
-
-/-- An element a of a commutative ring divides the additive inverse of an element b iff a
-  divides b. -/
-@[simp] lemma dvd_neg (a b : α) : (a ∣ -b) ↔ (a ∣ b) :=
-⟨dvd_of_dvd_neg, dvd_neg_of_dvd⟩
-
-/-- The additive inverse of an element a of a commutative ring divides another element b iff a
-  divides b. -/
-@[simp] lemma neg_dvd (a b : α) : (-a ∣ b) ↔ (a ∣ b) :=
-⟨dvd_of_neg_dvd, neg_dvd_of_dvd⟩
-
 /-- If an element a divides another element c in a commutative ring, a divides the sum of another
   element b with c iff a divides b. -/
 theorem dvd_add_left (h : a ∣ c) : a ∣ b + c ↔ a ∣ b :=
@@ -839,6 +806,56 @@ dvd_add_right (dvd_refl a)
 @[simp] lemma dvd_add_self_right {a b : α} : a ∣ b + a ↔ a ∣ b :=
 dvd_add_left (dvd_refl a)
 
+lemma dvd_iff_dvd_of_dvd_sub {a b c : α} (h : a ∣ (b - c)) : (a ∣ b ↔ a ∣ c) :=
+begin
+  split,
+  { intro h',
+    convert dvd_sub h' h,
+    exact eq.symm (sub_sub_self b c) },
+  { intro h',
+    convert dvd_add h h',
+    exact eq_add_of_sub_eq rfl }
+end
+
+@[simp] theorem even_neg (a : α) : even (-a) ↔ even a :=
+dvd_neg _ _
+
+end ring
+
+section comm_ring
+variables [comm_ring α] {a b c : α}
+
+/-- Pullback a `comm_ring` instance along an injective function.
+See note [reducible non-instances]. -/
+@[reducible]
+protected def function.injective.comm_ring
+  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
+  (f : β → α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+  (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) :
+  comm_ring β :=
+{ .. hf.ring f zero one add mul neg sub, .. hf.comm_semigroup f mul }
+
+/-- Pullback a `comm_ring` instance along an injective function.
+See note [reducible non-instances]. -/
+@[reducible]
+protected def function.surjective.comm_ring
+  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
+  (f : α → β) (hf : surjective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+  (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) :
+  comm_ring β :=
+{ .. hf.ring f zero one add mul neg sub, .. hf.comm_semigroup f mul }
+
+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
@@ -860,17 +877,6 @@ begin
   simp only [sub_eq_add_neg, add_assoc, neg_add_cancel_left],
 end
 
-lemma dvd_iff_dvd_of_dvd_sub {a b c : α} (h : a ∣ (b - c)) : (a ∣ b ↔ a ∣ c) :=
-begin
-  split,
-  { intro h',
-    convert dvd_sub h' h,
-    exact eq.symm (sub_sub_self b c) },
-  { intro h',
-    convert dvd_add h h',
-    exact eq_add_of_sub_eq rfl }
-end
-
 end comm_ring
 
 lemma succ_ne_self [ring α] [nontrivial α] (a : α) : a + 1 ≠ a :=
diff --git a/src/data/int/basic.lean b/src/data/int/basic.lean
index 242f5d30aa282..09f5ad8f75c83 100644
--- a/src/data/int/basic.lean
+++ b/src/data/int/basic.lean
@@ -730,10 +730,10 @@ begin
 end
 
 theorem nat_abs_dvd {a b : ℤ} : (a.nat_abs : ℤ) ∣ b ↔ a ∣ b :=
-(nat_abs_eq a).elim (λ e, by rw ← e) (λ e, by rw [← neg_dvd_iff_dvd, ← e])
+(nat_abs_eq a).elim (λ e, by rw ← e) (λ e, by rw [← neg_dvd, ← e])
 
 theorem dvd_nat_abs {a b : ℤ} : a ∣ b.nat_abs ↔ a ∣ b :=
-(nat_abs_eq b).elim (λ e, by rw ← e) (λ e, by rw [← dvd_neg_iff_dvd, ← e])
+(nat_abs_eq b).elim (λ e, by rw ← e) (λ e, by rw [← dvd_neg, ← e])
 
 instance decidable_dvd : @decidable_rel ℤ (∣) :=
 assume a n, decidable_of_decidable_of_iff (by apply_instance) (dvd_iff_mod_eq_zero _ _).symm
diff --git a/src/data/int/parity.lean b/src/data/int/parity.lean
index 99e5127c659ef..7c5184bc1a610 100644
--- a/src/data/int/parity.lean
+++ b/src/data/int/parity.lean
@@ -104,9 +104,6 @@ by rw [even_add, even_iff_not_odd, even_iff_not_odd, not_iff_not]
 theorem odd.add_odd (hm : odd m) (hn : odd n) : even (m + n) :=
 even_add'.2 $ iff_of_true hm hn
 
-@[parity_simps] theorem even_neg : even (-n) ↔ even n :=
-by simp [even_iff]
-
 @[simp] theorem not_even_bit1 (n : ℤ) : ¬ even (bit1 n) :=
 by simp [bit1] with parity_simps