fix(algebra/field): update to lean

algebra/field.lean

@@ -12,18 +12,9 @@ variables {α : Type u}
 section division_ring
 variables [division_ring α] {a b : α}
 
-lemma inv_ne_zero {a : α} (h : a ≠ 0) : a⁻¹ ≠ 0 :=
-by rw inv_eq_one_div; exact one_div_ne_zero h
-
-@[simp] lemma division_ring.inv_inv {a : α} (h : a ≠ 0) : a⁻¹⁻¹ = a :=
-by rw [inv_eq_one_div, inv_eq_one_div, division_ring.one_div_one_div h]
-
 lemma division_ring.inv_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : (a / b)⁻¹ = b / a :=
 by rw [division_def, mul_inv_eq (inv_ne_zero hb) ha, division_ring.inv_inv hb, division_def]
 
-lemma division_ring.one_div_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : 1 / (a / b) = b / a :=
-by rw [one_div_eq_inv, division_ring.inv_div ha hb]
-
 lemma division_ring.neg_inv (h : a ≠ 0) : - a⁻¹ = (- a)⁻¹ :=
 by rwa [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
 

algebra/ring.lean

@@ -18,6 +18,10 @@ end
 section
   variables [ring α] (a b c d e : α)
 
+  lemma mul_neg_one (a : α) : a * -1 = -a := by simp
+
+  lemma neg_one_mul (a : α) : -1 * a = -a := by simp
+
   theorem mul_add_eq_mul_add_iff_sub_mul_add_eq : a * e + c = b * e + d ↔ (a - b) * e + c = d :=
   calc
     a * e + c = b * e + d ↔ a * e + c = d + b * e : by simp
@@ -31,18 +35,11 @@ section
     (a - b) * e + c = (a * e + c) - b * e : begin simp [@sub_eq_add_neg α, @right_distrib α] end
                 ... = d                   : begin rewrite h, simp [@add_sub_cancel α] end
 
-  theorem mul_neg_one_eq_neg : a * (-1) = -a :=
-    have a + a * -1 = 0, from calc
-      a + a * -1 = a * 1 + a * -1 : by simp
-             ... = a * (1 + -1)   : eq.symm (left_distrib a 1 (-1))
-             ... = 0              : by simp,
-    (neg_eq_of_add_eq_zero this).symm
-
   theorem ne_zero_and_ne_zero_of_mul_ne_zero {a b : α} (h : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 :=
   begin
     split,
-      intro ha, apply h, simp [ha],
-    intro hb, apply h, simp [hb]
+    { intro ha, apply h, simp [ha] },
+    { intro hb, apply h, simp [hb] }
   end
 end