chore(algebra/invertible): generalise typeclasses (#13275)

src/algebra/invertible.lean

@@ -158,17 +158,18 @@ def invertible_one [monoid α] : invertible (1 : α) :=
 inv_of_eq_right_inv (mul_one _)
 
 /-- `-⅟a` is the inverse of `-a` -/
-def invertible_neg [ring α] (a : α) [invertible a] : invertible (-a) :=
-⟨ -⅟a, by simp, by simp ⟩
+def invertible_neg [has_mul α] [has_one α] [has_distrib_neg α] (a : α) [invertible a] :
+  invertible (-a) := ⟨-⅟a, by simp, by simp ⟩
 
-@[simp] lemma inv_of_neg [ring α] (a : α) [invertible a] [invertible (-a)] : ⅟(-a) = -⅟a :=
+@[simp] lemma inv_of_neg [monoid α] [has_distrib_neg α] (a : α) [invertible a] [invertible (-a)] :
+  ⅟(-a) = -⅟a :=
 inv_of_eq_right_inv (by simp)
 
 @[simp] lemma one_sub_inv_of_two [ring α] [invertible (2:α)] : 1 - (⅟2:α) = ⅟2 :=
 (is_unit_of_invertible (2:α)).mul_right_inj.1 $
   by rw [mul_sub, mul_inv_of_self, mul_one, bit0, add_sub_cancel]
 
-@[simp] lemma inv_of_two_add_inv_of_two [semiring α] [invertible (2 : α)] :
+@[simp] lemma inv_of_two_add_inv_of_two [non_assoc_semiring α] [invertible (2 : α)] :
   (⅟2 : α) + (⅟2 : α) = 1 :=
 by simp only [←two_mul, mul_inv_of_self]
 

src/algebra/ne_zero.lean

@@ -44,7 +44,7 @@ lemma of_gt  [canonically_ordered_add_monoid M] (h : x < y) : ne_zero y := of_po
 instance char_zero [ne_zero n] [add_monoid M] [has_one M] [char_zero M] : ne_zero (n : M) :=
 ⟨nat.cast_ne_zero.mpr $ ne_zero.ne n⟩
 
-@[priority 100] instance invertible [monoid_with_zero M] [nontrivial M] [invertible x] :
+@[priority 100] instance invertible [mul_zero_one_class M] [nontrivial M] [invertible x] :
   ne_zero x := ⟨nonzero_of_invertible x⟩
 
 instance coe_trans {r : R} [has_zero M] [has_coe R S] [has_coe_t S M] [h : ne_zero (r : M)] :