[Merged by Bors] - refactor(algebra/{group,group_with_zero/basic): Delete lemmas generalized to division monoids

archive/imo/imo2006_q3.lean

@@ -65,7 +65,7 @@ lemma zero_lt_32 : (0 : ℝ) < 32 := by norm_num
 
 theorem subst_wlog {x y z s : ℝ} (hxy : 0 ≤ x * y) (hxyz : x + y + z = 0) :
   32 * |x * y * z * s| ≤ sqrt 2 * (x^2 + y^2 + z^2 + s^2)^2 :=
-have hz : (x + y)^2 = z^2 := neg_eq_of_add_eq_zero hxyz ▸ (neg_sq _).symm,
+have hz : (x + y)^2 = z^2 := neg_eq_of_add_eq_zero_right hxyz ▸ (neg_sq _).symm,
 have hs : 0 ≤ 2 * s ^ 2 := mul_nonneg zero_le_two (sq_nonneg s),
 have this : _ :=
   calc  (2 * s^2) * (16 * x^2 * y^2 * (x + y)^2)

src/algebra/add_torsor.lean

@@ -128,7 +128,7 @@ end
 of subtracting them. -/
 @[simp] lemma neg_vsub_eq_vsub_rev (p1 p2 : P) : -(p1 -ᵥ p2) = (p2 -ᵥ p1) :=
 begin
-  refine neg_eq_of_add_eq_zero (vadd_right_cancel p1 _),
+  refine neg_eq_of_add_eq_zero_right (vadd_right_cancel p1 _),
   rw [vsub_add_vsub_cancel, vsub_self],
 end
 

src/algebra/big_operators/multiset.lean

@@ -211,7 +211,7 @@ by { convert (m.map f).prod_hom (comm_group.inv_monoid_hom : α →* α), rw map
 
 @[simp, to_additive]
 lemma prod_map_div : (m.map $ λ i, f i / g i).prod = (m.map f).prod / (m.map g).prod :=
-m.prod_hom₂ (/) mul_div_comm' (div_one' _) _ _
+m.prod_hom₂ (/) mul_div_mul_comm (div_one _) _ _
 
 @[to_additive]
 lemma prod_map_zpow {n : ℤ} : (m.map $ λ i, f i ^ n).prod = (m.map f).prod ^ n :=
@@ -234,7 +234,7 @@ by { convert (m.map f).prod_hom (inv_monoid_with_zero_hom : α →*₀ α), rw m
 
 @[simp]
 lemma prod_map_div₀ : (m.map $ λ i, f i / g i).prod = (m.map f).prod / (m.map g).prod :=
-m.prod_hom₂ (/) (λ _ _ _ _, (div_mul_div_comm₀ _ _ _ _).symm) (div_one _) _ _
+m.prod_hom₂ (/) (λ _ _ _ _, (div_mul_div_comm _ _ _ _).symm) (div_one _) _ _
 
 lemma prod_map_zpow₀ {n : ℤ} : prod (m.map $ λ i, f i ^ n) = (m.map f).prod ^ n :=
 by { convert (m.map f).prod_hom (zpow_group_hom₀ _ : α →* α), rw map_map, refl }

src/algebra/field/basic.lean

@@ -70,7 +70,7 @@ local attribute [simp]
 
 lemma one_div_neg_one_eq_neg_one : (1:K) / (-1) = -1 :=
 have (-1) * (-1) = (1:K), by rw [neg_mul_neg, one_mul],
-eq.symm (eq_one_div_of_mul_eq_one this)
+eq.symm (eq_one_div_of_mul_eq_one_right this)
 
 lemma one_div_neg_eq_neg_one_div (a : K) : 1 / (- a) = - (1 / a) :=
 calc

src/algebra/geom_sum.lean

@@ -343,7 +343,7 @@ have h₂ : x⁻¹ - 1 ≠ 0, from mt sub_eq_zero.1 h₁,
 have h₃ : x - 1 ≠ 0, from mt sub_eq_zero.1 hx1,
 have h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x :=
   nat.rec_on n (by simp)
-  (λ n h, by rw [pow_succ, mul_inv_rev₀, ←mul_assoc, h, mul_assoc, mul_inv_cancel hx0, mul_assoc,
+  (λ n h, by rw [pow_succ, mul_inv_rev, ←mul_assoc, h, mul_assoc, mul_inv_cancel hx0, mul_assoc,
     inv_mul_cancel hx0]),
 begin
   rw [geom_sum_eq h₁, div_eq_iff_mul_eq h₂, ← mul_right_inj' h₃,
@@ -467,7 +467,7 @@ begin
   { have := geom_sum_alternating_of_lt_neg_one hx k.one_lt_succ_succ,
     simp only [h, if_false] at this,
     exact zero_lt_one.trans this },
-  { simp only [eq_neg_of_add_eq_zero hx, h, neg_one_geom_sum, if_false, zero_lt_one] },
+  { simp only [eq_neg_of_add_eq_zero_left hx, h, neg_one_geom_sum, if_false, zero_lt_one] },
   rcases lt_trichotomy x 0 with hx' | rfl | hx',
   { exact (geom_sum_pos_and_lt_one hx' hx k.one_lt_succ_succ).1 },
   { simp only [zero_geom_sum, nat.succ_ne_zero, if_false, zero_lt_one] },

src/algebra/group/basic.lean

@@ -220,16 +220,15 @@ lemma mul_div_assoc' (a b c : G) : a * (b / c) = (a * b) / c :=
 @[simp, to_additive] lemma one_div (a : G) : 1 / a = a⁻¹ :=
 (inv_eq_one_div a).symm
 
-@[to_additive]
-lemma mul_div (a b c : G) : a * (b / c) = a * b / c :=
+@[to_additive] lemma mul_div (a b c : G) : a * (b / c) = a * b / c :=
 by simp only [mul_assoc, div_eq_mul_inv]
 
 @[to_additive] lemma div_eq_mul_one_div (a b : G) : a / b = a * (1 / b) :=
 by rw [div_eq_mul_inv, one_div]
 
 end div_inv_monoid
 
-namespace division_monoid
+section division_monoid
 variables [division_monoid α] {a b c : α}
 
 local attribute [simp] mul_assoc div_eq_mul_inv
@@ -285,21 +284,22 @@ by simp only [mul_assoc, mul_inv_rev, div_eq_mul_inv]
 
 end division_monoid
 
-namespace division_comm_monoid
+section division_comm_monoid
 variables [division_comm_monoid α] (a b c d : α)
 
 local attribute [simp] mul_assoc mul_comm mul_left_comm div_eq_mul_inv
 
 @[to_additive neg_add] lemma mul_inv : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by simp
+@[to_additive] lemma inv_div' : (a / b)⁻¹ = a⁻¹ / b⁻¹ := by simp
 @[to_additive] lemma div_eq_inv_mul : a / b = b⁻¹ * a := by simp
 @[to_additive] lemma inv_mul_eq_div : a⁻¹ * b = b / a := by simp
 @[to_additive] lemma inv_mul' : (a * b)⁻¹ = a⁻¹ / b := by simp
-@[to_additive] lemma inv_div_inv : (a⁻¹ / b⁻¹) = b / a := by simp
+@[simp, to_additive] lemma inv_div_inv : (a⁻¹ / b⁻¹) = b / a := by simp
 @[to_additive] lemma inv_inv_div_inv : (a⁻¹ / b⁻¹)⁻¹ = a / b := by simp
 @[to_additive] lemma one_div_mul_one_div : (1 / a) * (1 / b) =  1 / (a * b) := by simp
 
 @[to_additive] lemma div_right_comm : a / b / c = a / c / b := by simp
-@[to_additive] lemma div_div : a / b / c = a / (b * c) := by simp
+@[to_additive, field_simps] lemma div_div : a / b / c = a / (b * c) := by simp
 @[to_additive] lemma div_mul : a / b * c = a / (b / c) := by simp
 @[to_additive] lemma mul_div_left_comm : a * (b / c) = b * (a / c) := by simp
 @[to_additive] lemma mul_div_right_comm : a * b / c = a / c * b := by simp
@@ -319,12 +319,6 @@ end division_comm_monoid
 section group
 variables [group G] {a b c d : G}
 
-@[to_additive neg_zero] lemma one_inv : 1⁻¹ = (1 : G) := division_monoid.inv_one
-
-@[to_additive] theorem inv_eq_one : a⁻¹ = 1 ↔ a = 1 := division_monoid.inv_eq_one
-@[to_additive] theorem one_eq_inv : 1 = a⁻¹ ↔ a = 1 := division_monoid.one_eq_inv
-@[to_additive] theorem inv_ne_one : a⁻¹ ≠ 1 ↔ a ≠ 1 := division_monoid.inv_ne_one
-
 @[simp, to_additive] theorem div_eq_inv_self : a / b = b⁻¹ ↔ a = 1 :=
 by rw [div_eq_mul_inv, mul_left_eq_self]
 
@@ -336,9 +330,6 @@ theorem mul_left_surjective (a : G) : function.surjective ((*) a) :=
 theorem mul_right_surjective (a : G) : function.surjective (λ x, x * a) :=
 λ x, ⟨x * a⁻¹, inv_mul_cancel_right x a⟩
 
-@[to_additive]
-lemma eq_inv_of_mul_eq_one : a * b = 1 → a = b⁻¹ := division_monoid.eq_inv_of_mul_eq_one_left
-
 @[to_additive]
 lemma eq_mul_inv_of_mul_eq (h : a * c = b) : a = b * c⁻¹ :=
 by simp [h.symm]
@@ -373,7 +364,7 @@ by simp [h]
 
 @[to_additive]
 theorem mul_eq_one_iff_eq_inv : a * b = 1 ↔ a = b⁻¹ :=
-⟨eq_inv_of_mul_eq_one, λ h, by rw [h, mul_left_inv]⟩
+⟨eq_inv_of_mul_eq_one_left, λ h, by rw [h, mul_left_inv]⟩
 
 @[to_additive]
 theorem mul_eq_one_iff_inv_eq : a * b = 1 ↔ a⁻¹ = b :=
@@ -419,9 +410,6 @@ by simpa only [div_eq_mul_inv] using λ a a' h, mul_left_injective (b⁻¹) h
 lemma div_right_injective : function.injective (λ a, b / a) :=
 by simpa only [div_eq_mul_inv] using λ a a' h, inv_injective (mul_right_injective b h)
 
-@[to_additive neg_sub]
-lemma inv_div' (a b : G) : (a / b)⁻¹ = b / a := division_monoid.inv_div _ _
-
 @[simp, to_additive sub_add_cancel]
 lemma div_mul_cancel' (a b : G) : a / b * b = a :=
 by rw [div_eq_mul_inv, inv_mul_cancel_right a b]
@@ -434,18 +422,6 @@ by rw [div_eq_mul_inv, mul_right_inv a]
 lemma mul_div_cancel'' (a b : G) : a * b / b = a :=
 by rw [div_eq_mul_inv, mul_inv_cancel_right a b]
 
-@[to_additive eq_of_sub_eq_zero]
-lemma eq_of_div_eq_one' : a / b = 1 → a = b := division_monoid.eq_of_div_eq_one
-
-@[to_additive] lemma div_ne_one_of_ne : a ≠ b → a / b ≠ 1 := division_monoid.div_ne_one_of_ne
-
-@[to_additive]
-lemma div_inv_eq_mul (a b : G) : a / (b⁻¹) = a * b := division_monoid.div_inv_eq_mul _ _
-
-@[to_additive]
-lemma div_mul_eq_div_div_swap (a b c : G) : a / (b * c) = a / c / b :=
-division_monoid.div_mul_eq_div_div_swap _ _ _
-
 @[simp, to_additive]
 lemma mul_div_mul_right_eq_div (a b c : G) : (a * c) / (b * c) = a / b :=
 by rw [div_mul_eq_div_div_swap]; simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel'']
@@ -480,14 +456,11 @@ by rw [← mul_div_assoc, div_mul_cancel']
 
 @[simp, to_additive sub_sub_sub_cancel_right]
 lemma div_div_div_cancel_right' (a b c : G) : (a / c) / (b / c) = a / b :=
-by rw [← inv_div' c b, div_inv_eq_mul, div_mul_div_cancel']
-
-@[to_additive]
-theorem div_div_assoc_swap : a / (b / c) = a * c / b := division_monoid.div_div_eq_mul_div _ _ _
+by rw [← inv_div c b, div_inv_eq_mul, div_mul_div_cancel']
 
 @[to_additive]
 theorem div_eq_one : a / b = 1 ↔ a = b :=
-⟨eq_of_div_eq_one', λ h, by rw [h, div_self']⟩
+⟨eq_of_div_eq_one, λ h, by rw [h, div_self']⟩
 
 alias div_eq_one ↔ _ div_eq_one_of_eq
 alias sub_eq_zero ↔ _ sub_eq_zero_of_eq
@@ -500,10 +473,6 @@ not_congr div_eq_one
 theorem div_eq_self : a / b = a ↔ b = 1 :=
 by rw [div_eq_mul_inv, mul_right_eq_self, inv_eq_one]
 
--- The unprimed version is used by `group_with_zero`.  This is the preferred choice.
--- See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60div_one'.60
-@[to_additive sub_zero] lemma div_one' (a : G) : a / 1 = a := division_monoid.div_one _
-
 @[to_additive eq_sub_iff_add_eq]
 theorem eq_div_iff_mul_eq' : a = b / c ↔ a * c = b :=
 by rw [div_eq_mul_inv, eq_mul_inv_iff_mul_eq]
@@ -552,42 +521,10 @@ variables [comm_group G] {a b c d : G}
 
 local attribute [simp] mul_assoc mul_comm mul_left_comm div_eq_mul_inv
 
-@[to_additive neg_add]
-lemma mul_inv (a b : G) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := division_comm_monoid.mul_inv _ _
-
 @[to_additive]
 lemma div_eq_of_eq_mul' {a b c : G} (h : a = b * c) : a / b = c :=
 by rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
 
-@[to_additive]
-lemma mul_div_left_comm {x y z : G} : x * (y / z) = y * (x / z) :=
-division_comm_monoid.mul_div_left_comm _ _ _
-
-@[to_additive]
-lemma div_mul_div_comm (a b c d : G) : a / b * (c / d) = a * c / (b * d) :=
-division_comm_monoid.div_mul_div_comm _ _ _ _
-
-@[to_additive]
-lemma div_div_div_comm (a b c d : G) : (a / b) / (c / d) = (a / c) / (b / d) :=
-division_comm_monoid.div_div_div_comm _ _ _ _
-
-@[to_additive]
-lemma div_mul_eq_div_div (a b c : G) : a / (b * c) = a / b / c :=
-division_comm_monoid.div_mul_eq_div_div _ _ _
-
-@[to_additive]
-lemma inv_mul_eq_div (a b : G) : a⁻¹ * b = b / a := division_comm_monoid.inv_mul_eq_div _ _
-
-@[to_additive sub_add_eq_add_sub]
-lemma div_mul_eq_mul_div' (a b c : G) : a / b * c = a * c / b :=
-division_comm_monoid.div_mul_eq_mul_div _ _ _
-
-@[to_additive]
-lemma div_div (a b c : G) : a / b / c = a / (b * c) := division_comm_monoid.div_div _ _ _
-
-@[to_additive]
-lemma div_mul (a b c : G) : a / b * c = a / (b / c) := division_comm_monoid.div_mul _ _ _
-
 @[simp, to_additive]
 lemma mul_div_mul_left_eq_div (a b c : G) : (c * a) / (c * b) = a / b :=
 by simp
@@ -608,31 +545,15 @@ begin simp [h], rw [mul_comm c, mul_inv_cancel_left] end
 lemma div_div_self' (a b : G) : a / (a / b) = b :=
 by simpa using mul_inv_cancel_left a b
 
-@[to_additive add_sub_comm]
-lemma mul_div_comm' (a b c d : G) : a * b / (c * d) = (a / c) * (b / d) :=
-division_comm_monoid.mul_div_mul_comm _ _ _ _
-
 @[to_additive]
 lemma div_eq_div_mul_div (a b c : G) : a / b = c / b * (a / c) := by simp [mul_left_comm c]
 
-@[to_additive]
-lemma inv_inv_div_inv (a b : G) : (a⁻¹ / b⁻¹)⁻¹ = a / b := division_comm_monoid.inv_inv_div_inv _ _
-
 @[simp, to_additive]
 lemma div_div_cancel (a b : G) : a / (a / b) = b := div_div_self' a b
 
-@[to_additive sub_eq_neg_add]
-lemma div_eq_inv_mul' (a b : G) : a / b = b⁻¹ * a := division_comm_monoid.div_eq_inv_mul _ _
-
 @[simp, to_additive]
 lemma div_div_cancel_left (a b : G) : a / b / a = b⁻¹ := by simp
 
-@[to_additive]
-theorem inv_mul' (a b : G) : (a * b)⁻¹ = a⁻¹ / b := division_comm_monoid.inv_mul' _ _
-
-@[simp, to_additive]
-lemma inv_div_inv (a b : G) : a⁻¹ / b⁻¹ = b / a := division_comm_monoid.inv_div_inv _ _
-
 @[to_additive eq_sub_iff_add_eq']
 lemma eq_div_iff_mul_eq'' : a = b / c ↔ c * a = b :=
 by rw [eq_div_iff_mul_eq', mul_comm]
@@ -642,16 +563,15 @@ lemma div_eq_iff_eq_mul' : a / b = c ↔ a = b * c :=
 by rw [div_eq_iff_eq_mul, mul_comm]
 
 @[simp, to_additive add_sub_cancel']
-lemma mul_div_cancel''' (a b : G) : a * b / a = b :=
-by rw [div_eq_inv_mul', inv_mul_cancel_left]
+lemma mul_div_cancel''' (a b : G) : a * b / a = b := by rw [div_eq_inv_mul, inv_mul_cancel_left]
 
 @[simp, to_additive]
 lemma mul_div_cancel'_right (a b : G) : a * (b / a) = b :=
 by rw [← mul_div_assoc, mul_div_cancel''']
 
 @[simp, to_additive sub_add_cancel']
 lemma div_mul_cancel'' (a b : G) : a / (a * b) = b⁻¹ :=
-by rw [← inv_div', mul_div_cancel''']
+by rw [← inv_div, mul_div_cancel''']
 
 -- This lemma is in the `simp` set under the name `mul_inv_cancel_comm_assoc`,
 -- along with the additive version `add_neg_cancel_comm_assoc`,
@@ -660,10 +580,6 @@ by rw [← inv_div', mul_div_cancel''']
 lemma mul_mul_inv_cancel'_right (a b : G) : a * (b * a⁻¹) = b :=
 by rw [← div_eq_mul_inv, mul_div_cancel'_right a b]
 
-@[to_additive sub_right_comm]
-lemma div_right_comm' (a b c : G) : a / b / c = a / c / b :=
-division_comm_monoid.div_right_comm _ _ _
-
 @[simp, to_additive]
 lemma mul_mul_div_cancel (a b c : G) : (a * c) * (b / c) = a * b :=
 by rw [mul_assoc, mul_div_cancel'_right]
@@ -682,16 +598,16 @@ by rw [← div_mul, mul_div_cancel''']
 
 @[simp, to_additive]
 lemma div_div_div_cancel_left (a b c : G) : (c / a) / (c / b) = b / a :=
-by rw [← inv_div' b c, div_inv_eq_mul, mul_comm, div_mul_div_cancel']
+by rw [← inv_div b c, div_inv_eq_mul, mul_comm, div_mul_div_cancel']
 
 @[to_additive] lemma div_eq_div_iff_mul_eq_mul : a / b = c / d ↔ a * d = c * b :=
 begin
-  rw [div_eq_iff_eq_mul, div_mul_eq_mul_div', eq_comm, div_eq_iff_eq_mul'],
+  rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul'],
   simp only [mul_comm, eq_comm]
 end
 
 @[to_additive] lemma div_eq_div_iff_div_eq_div : a / b = c / d ↔ a / c = b / d :=
-by rw [div_eq_iff_eq_mul, div_mul_eq_mul_div', div_eq_iff_eq_mul', mul_div_assoc]
+by rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, div_eq_iff_eq_mul', mul_div_assoc]
 
 end comm_group
 

src/algebra/group/defs.lean

@@ -688,9 +688,6 @@ division_monoid.mul_inv_rev _ _
 @[to_additive]
 lemma inv_eq_of_mul_eq_one_right : a * b = 1 → a⁻¹ = b := division_monoid.inv_eq_of_mul _ _
 
-@[simp, to_additive]
-lemma inv_eq_of_mul_eq_one : a * b = 1 → a⁻¹ = b := division_monoid.inv_eq_of_mul _ _
-
 end division_monoid
 
 /-- Commutative `subtraction_monoid`. -/

src/algebra/group/inj_surj.lean

@@ -218,7 +218,7 @@ protected def division_monoid [division_monoid M₂] (f : M₁ → M₂) (hf : i
   (zpow : ∀ x (n : ℤ), f (x ^ n) = f x ^ n) :
   division_monoid M₁ :=
 { mul_inv_rev := λ x y, hf $ by erw [inv, mul, mul_inv_rev, mul, inv, inv],
-  inv_eq_of_mul := λ x y h, hf $ by erw [inv, inv_eq_of_mul_eq_one (by erw [←mul, h, one])],
+  inv_eq_of_mul := λ x y h, hf $ by erw [inv, inv_eq_of_mul_eq_one_right (by erw [←mul, h, one])],
   ..hf.div_inv_monoid f one mul inv div npow zpow, ..hf.has_involutive_inv f inv  }
 
 /-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `division_comm_monoid`

src/algebra/group/prod.lean

@@ -139,8 +139,8 @@ instance [div_inv_monoid G] [div_inv_monoid H] : div_inv_monoid (G × H) :=
 @[to_additive subtraction_monoid]
 instance [division_monoid G] [division_monoid H] : division_monoid (G × H) :=
 { mul_inv_rev := λ a b, ext (mul_inv_rev _ _) (mul_inv_rev _ _),
-  inv_eq_of_mul := λ a b h, ext (inv_eq_of_mul_eq_one $ congr_arg fst h)
-    (inv_eq_of_mul_eq_one $ congr_arg snd h),
+  inv_eq_of_mul := λ a b h, ext (inv_eq_of_mul_eq_one_right $ congr_arg fst h)
+    (inv_eq_of_mul_eq_one_right $ congr_arg snd h),
   .. prod.div_inv_monoid, .. prod.has_involutive_inv }
 
 @[to_additive subtraction_comm_monoid]
@@ -478,7 +478,7 @@ Used mainly to define the natural topology of `αˣ`. -/
 Used mainly to define the natural topology of `add_units α`."]
 def embed_product (α : Type*) [monoid α] : αˣ →* α × αᵐᵒᵖ :=
 { to_fun := λ x, ⟨x, op ↑x⁻¹⟩,
-  map_one' := by simp only [one_inv, eq_self_iff_true, units.coe_one, op_one, prod.mk_eq_one,
+  map_one' := by simp only [inv_one, eq_self_iff_true, units.coe_one, op_one, prod.mk_eq_one,
     and_self],
   map_mul' := λ x y, by simp only [mul_inv_rev, op_mul, units.coe_mul, prod.mk_mul_mk] }
 
@@ -511,15 +511,15 @@ def mul_monoid_with_zero_hom [comm_monoid_with_zero α] : α × α →*₀ α :=
 @[to_additive "Subtraction as an additive monoid homomorphism.", simps]
 def div_monoid_hom [comm_group α] : α × α →* α :=
 { to_fun := λ a, a.1 / a.2,
-  map_one' := div_one' _,
-  map_mul' := λ a b, mul_div_comm' _ _ _ _ }
+  map_one' := div_one _,
+  map_mul' := λ a b, mul_div_mul_comm _ _ _ _ }
 
 /-- Division as a multiplicative homomorphism with zero. -/
 @[simps]
 def div_monoid_with_zero_hom [comm_group_with_zero α] : α × α →*₀ α :=
 { to_fun := λ a, a.1 / a.2,
   map_zero' := zero_div _,
   map_one' := div_one _,
-  map_mul' := λ a b, (div_mul_div_comm₀ _ _ _ _).symm }
+  map_mul' := λ a b, mul_div_mul_comm _ _ _ _ }
 
 end bundled_mul_div

src/algebra/group/type_tags.lean

@@ -253,12 +253,12 @@ instance [sub_neg_monoid α] : div_inv_monoid (multiplicative α) :=
 
 instance [division_monoid α] : subtraction_monoid (additive α) :=
 { neg_add_rev := @mul_inv_rev _ _,
-  neg_eq_of_add := @inv_eq_of_mul_eq_one _ _,
+  neg_eq_of_add := @inv_eq_of_mul_eq_one_right _ _,
   .. additive.sub_neg_monoid, .. additive.has_involutive_neg }
 
 instance [subtraction_monoid α] : division_monoid (multiplicative α) :=
 { mul_inv_rev := @neg_add_rev _ _,
-  inv_eq_of_mul := @neg_eq_of_add_eq_zero _ _,
+  inv_eq_of_mul := @neg_eq_of_add_eq_zero_right _ _,
   .. multiplicative.div_inv_monoid, .. multiplicative.has_involutive_inv }
 
 instance [division_comm_monoid α] : subtraction_comm_monoid (additive α) :=