chore(algebra/field): deduplicate with group_with_zero (#3015)

For historical reasons there are lots of lemmas we prove for `group_with_zero`, then again for a `division_ring`. Merge some of them.



Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/algebra/continued_fractions/convergents_equiv.lean

@@ -318,7 +318,7 @@ begin
         { simp [*, (continuants_aux_eq_continuants_aux_squash_gcf_of_le $ le_refl $ n' + 1).symm,
             (continuants_aux_eq_continuants_aux_squash_gcf_of_le n'.le_succ).symm] },
         symmetry,
-        simpa only [eq1, eq2, eq3, eq4, mul_div_cancel'' _  b_ne_zero] },
+        simpa only [eq1, eq2, eq3, eq4, mul_div_cancel _  b_ne_zero] },
       field_simp [b_ne_zero],
       congr' 1; ring } }
 end

src/algebra/field.lean

@@ -29,75 +29,26 @@ instance division_ring.to_nonzero : nonzero α :=
 instance division_ring_has_div : has_div α :=
 ⟨λ a b, a * b⁻¹⟩
 
-lemma division_def (a b : α) : a / b = a * b⁻¹ :=
-rfl
-
-@[simp] lemma mul_inv_cancel (h : a ≠ 0) : a * a⁻¹ = 1 :=
-division_ring.mul_inv_cancel h
-
-@[simp] lemma inv_mul_cancel (h : a ≠ 0) : a⁻¹ * a = 1 :=
-division_ring.inv_mul_cancel h
+/-- Every division ring is a `group_with_zero`. -/
+@[priority 100] -- see Note [lower instance priority]
+instance division_ring.to_group_with_zero :
+  group_with_zero α :=
+{ .. ‹division_ring α›,
+  .. (infer_instance : semiring α) }
 
 @[simp] lemma one_div_eq_inv (a : α) : 1 / a = a⁻¹ := one_mul a⁻¹
 
 @[field_simps] lemma inv_eq_one_div (a : α) : a⁻¹ = 1 / a := by simp
 
-/-- Every division ring is a `group_with_zero`. -/
-@[priority 10] -- see Note [lower instance priority]
-instance division_ring.to_group_with_zero :
-  group_with_zero α :=
-{ mul_inv_cancel := λ _, mul_inv_cancel,
-  .. ‹division_ring α›,
-  .. (by apply_instance : semiring α) }
-
 local attribute [simp]
   division_def mul_comm mul_assoc
   mul_left_comm mul_inv_cancel inv_mul_cancel
 
-lemma div_eq_mul_one_div (a b : α) : a / b = a * (1 / b) := by simp
-
-lemma mul_one_div_cancel (h : a ≠ 0) : a * (1 / a) = 1 := by simp [h]
-
-lemma one_div_mul_cancel (h : a ≠ 0) : (1 / a) * a = 1 := by simp [h]
-
-@[simp] lemma div_self (h : a ≠ 0) : a / a = 1 := by simp [h]
-
-lemma one_div_one : 1 / 1 = (1:α) :=
-div_self (ne.symm zero_ne_one)
-
-theorem inv_one : (1⁻¹ : α) = 1 := by rw [inv_eq_one_div, one_div_one]
-
-lemma mul_div_assoc (a b c : α) : (a * b) / c = a * (b / c) := by simp
-
 @[field_simps] lemma mul_div_assoc' (a b c : α) : a * (b / c) = (a * b) / c :=
 by simp [mul_div_assoc]
 
-lemma one_div_ne_zero (h : a ≠ 0) : 1 / a ≠ 0 :=
-assume : 1 / a = 0,
-have 0 = (1:α), from eq.symm (by rw [← mul_one_div_cancel h, this, mul_zero]),
-absurd this zero_ne_one
-
-lemma ne_zero_of_one_div_ne_zero (h : 1 / a ≠ 0) : a ≠ 0 :=
-assume ha : a = 0, begin rw [ha, div_zero] at h, contradiction end
-
-lemma inv_ne_zero (h : a ≠ 0) : a⁻¹ ≠ 0 :=
-by rw inv_eq_one_div; exact one_div_ne_zero h
-
-lemma eq_zero_of_one_div_eq_zero (h : 1 / a = 0) : a = 0 :=
-classical.by_cases
-  (assume ha, ha)
-  (assume ha, false.elim ((one_div_ne_zero ha) h))
-
-lemma one_inv_eq : 1⁻¹ = (1:α) :=
-calc 1⁻¹ = 1 * 1⁻¹ : by rw [one_mul]
-     ... = (1:α)   : by simp
-
 local attribute [simp] one_inv_eq
 
-lemma div_one (a : α) : a / 1 = a := by simp
-
-lemma zero_div (a : α) : 0 / a = 0 := by simp
-
 -- note: integral domain has a "mul_ne_zero". a commutative division ring is an integral
 -- domain, but let's not define that class for now.
 lemma division_ring.mul_ne_zero (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 :=
@@ -182,25 +133,6 @@ lemma one_div_div (a b : α) : 1 / (a / b) = b / a :=
 by rw [one_div_eq_inv, division_def, mul_inv',
        inv_inv', division_def]
 
-lemma div_helper (b : α) (h : a ≠ 0) : (1 / (a * b)) * a = 1 / b :=
-by simp only [division_def, mul_inv', one_mul, mul_assoc, inv_mul_cancel h, mul_one]
-
-lemma mul_div_cancel (a : α) {b : α} (hb : b ≠ 0) : a * b / b = a :=
-by simp [hb]
-
-lemma div_mul_cancel (a : α) {b : α} (hb : b ≠ 0) : a / b * b = a :=
-by simp [hb]
-
-@[field_simps] lemma div_div_eq_mul_div (a b c : α) : a / (b / c) = (a * c) / b :=
-by rw [div_eq_mul_one_div, one_div_div, ← mul_div_assoc]
-
-lemma div_mul_left (hb : b ≠ 0) : b / (a * b) = 1 / a :=
-by simp only [division_def, mul_inv', ← mul_assoc, mul_inv_cancel hb]
-
-lemma mul_div_mul_right (a : α) (b : α) {c : α} (hc : c ≠ 0) :
-      (a * c) / (b * c) = a / b :=
-by rw [mul_div_assoc, div_mul_left hc, ← mul_div_assoc, mul_one]
-
 @[field_simps] lemma div_add_div_same (a b c : α) : a / c + b / c = (a + b) / c :=
 eq.symm $ right_distrib a b (c⁻¹)
 
@@ -267,12 +199,6 @@ have (a + b / c) * c = a * c + b, by rw [right_distrib, (div_mul_cancel _ hc)],
 lemma mul_mul_div (a : α) {c : α} (hc : c ≠ 0) : a = a * c * (1 / c) :=
 by simp [hc]
 
-lemma eq_of_mul_eq_mul_of_nonzero_left {a b c : α} (h : a ≠ 0) (h₂ : a * b = a * c) : b = c :=
-by rw [← one_mul b, ← inv_mul_cancel h, mul_assoc, h₂, ← mul_assoc, inv_mul_cancel h, one_mul]
-
-lemma eq_of_mul_eq_mul_of_nonzero_right {a b c : α} (h : c ≠ 0) (h2 : a * c = b * c) : a = b :=
-by rw [← mul_one a, ← mul_inv_cancel h, ← mul_assoc, h2, mul_assoc, mul_inv_cancel h, mul_one]
-
 instance division_ring.to_domain : domain α :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ a b h,
     classical.by_contradiction $ λ hn,
@@ -295,45 +221,21 @@ instance field.to_division_ring : division_ring α :=
 { inv_mul_cancel := λ _ h, by rw [mul_comm, field.mul_inv_cancel h]
   ..show field α, by apply_instance }
 
-lemma one_div_mul_one_div (a b : α) : (1 / a) * (1 / b) =  1 / (a * b) :=
-by rw [division_ring.one_div_mul_one_div, mul_comm b]
-
-lemma div_mul_right {a : α} (b : α) (ha : a ≠ 0) : a / (a * b) = 1 / b :=
-by rw [mul_comm, div_mul_left ha]
-
-lemma mul_div_cancel_left {a : α} (b : α) (ha : a ≠ 0) : a * b / a = b :=
-by rw [mul_comm a, (mul_div_cancel _ ha)]
-
-lemma mul_div_cancel' (a : α) {b : α} (hb : b ≠ 0) : b * (a / b) = a :=
-by rw [mul_comm, (div_mul_cancel _ hb)]
+/-- Every field is a `comm_group_with_zero`. -/
+instance field.to_comm_group_with_zero :
+  comm_group_with_zero α :=
+{ .. (_ : group_with_zero α), .. ‹field α› }
 
 lemma one_div_add_one_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) :=
 by rw [add_comm, ← div_mul_left ha, ← div_mul_right _ hb,
        division_def, division_def, division_def, ← right_distrib, mul_comm a]
 
 local attribute [simp] mul_assoc mul_comm mul_left_comm
 
-lemma div_mul_div (a b c d : α) :
-      (a / b) * (c / d) = (a * c) / (b * d) :=
-begin simp [division_def], rw [mul_inv', mul_comm d⁻¹] end
-
-lemma mul_div_mul_left (a b : α) {c : α} (hc : c ≠ 0) :
-      (c * a) / (c * b) = a / b :=
-by rw [← div_mul_div, div_self hc, one_mul]
-
-@[field_simps] lemma div_mul_eq_mul_div (a b c : α) : (b / c) * a = (b * a) / c :=
-by simp [division_def]
-
-lemma div_mul_eq_mul_div_comm (a b c : α) :
-      (b / c) * a = b * (a / c) :=
-by rw [div_mul_eq_mul_div, ← one_mul c, ← div_mul_div,
-       div_one, one_mul]
-
 lemma div_add_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) :
       (a / b) + (c / d) = ((a * d) + (b * c)) / (b * d) :=
 by rw [← mul_div_mul_right _ b hd, ← mul_div_mul_left c d hb, div_add_div_same]
 
-
 @[field_simps] lemma div_sub_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) :
   (a / b) - (c / d) = ((a * d) - (b * c)) / (b * d) :=
 begin
@@ -342,23 +244,6 @@ begin
       ← mul_assoc, mul_comm b, mul_assoc, ← neg_eq_neg_one_mul]
 end
 
-lemma mul_eq_mul_of_div_eq_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0)
-  (hd : d ≠ 0) (h : a / b = c / d) : a * d = c * b :=
-by rw [← mul_one (a*d), mul_assoc, mul_comm d, ← mul_assoc, ← div_self hb,
-       ← div_mul_eq_mul_div_comm, h, div_mul_eq_mul_div, div_mul_cancel _ hd]
-
-@[field_simps] lemma div_div_eq_div_mul (a b c : α) : (a / b) / c = a / (b * c) :=
-by rw [div_eq_mul_one_div, div_mul_div, mul_one]
-
-lemma div_div_div_div_eq (a : α) {b c d : α} :
-      (a / b) / (c / d) = (a * d) / (b * c) :=
-by rw [div_div_eq_mul_div, div_mul_eq_mul_div,
-       div_div_eq_div_mul]
-
-lemma div_mul_eq_div_mul_one_div (a b c : α) :
-      a / (b * c) = (a / b) * (1 / c) :=
-by rw [← div_div_eq_div_mul, ← div_eq_mul_one_div]
-
 lemma inv_add_inv {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = (a + b) / (a * b) :=
 by rw [inv_eq_one_div, inv_eq_one_div, one_div_add_one_div ha hb]
 
@@ -377,11 +262,6 @@ by rwa [add_comm, add_div', add_comm]
 @[field_simps] lemma div_sub' (a b c : α) (hc : c ≠ 0) : a / c - b = (a - c * b) / c :=
 by simpa using div_sub_div a b hc one_ne_zero
 
-/-- Every field is a `comm_group_with_zero`. -/
-instance field.to_comm_group_with_zero :
-  comm_group_with_zero α :=
-{ .. (_ : group_with_zero α), .. ‹field α› }
-
 @[priority 100] -- see Note [lower instance priority]
 instance field.to_integral_domain : integral_domain α :=
 { ..‹field α›, ..division_ring.to_domain }