feat(Algebra/Group/Defs): add DivInvMonoid (#7)

* feat(Algebra/*): beginning of algebra heirarchy

* update -- instance Ring to Semiring now working

* add group proofs

* now finished everything in Sebastien's suggested list

* feat(Mathlib/Algebra/Group): add DivInvMonoid and SubNegMonoid

* add comment

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Mathlib/Algebra/Group/Defs.lean

@@ -192,17 +192,30 @@ instance (A : Type u) [AddCommMonoid A] : AddCommSemigroup A where
 
 /-
 
+### sub_neg_monoids
+
+Additive groups can "pick up" several equal but not defeq actions of ℤ.
+This trick isolates one such action, `gsmul`, and decrees it to
+be "the canonical one".
+
+-/
+
+class SubNegMonoid (A : Type u) extends AddMonoid A, Neg A, Sub A :=
+(sub := λ a b => a + -b)
+(sub_eq_add_neg : ∀ a b : A, a - b = a + -b)
+(gsmul : ℤ → A → A := gsmul_rec)
+(gsmul_zero' : ∀ (a : A), gsmul 0 a = 0)
+(gpow_succ' (n : ℕ) (a : A) : gsmul (Int.ofNat n.succ) a = a + gsmul (Int.ofNat n) a)
+(gpow_neg' (n : ℕ) (a : A) : gsmul (Int.negSucc n) a = -(gsmul ↑(n.succ) a))
+
+/-
+
 ### Additive groups
 
 -/
 
-class AddGroup (A : Type u) extends AddMonoid A, Neg A, Sub A where
+class AddGroup (A : Type u) extends SubNegMonoid A where
   add_left_neg (a : A) : -a + a = 0
-  sub_eq_add_neg (a b : A) : a - b = a + -b 
-  gsmul : ℤ → A → A := gsmul_rec
-  gpow_zero' (a : A) : gsmul 0 a = 0 -- try rfl
-  gpow_succ' (n : ℕ) (a : A) : gsmul (Int.ofNat n.succ) a = a + gsmul (Int.ofNat n) a 
-  gpow_neg' (n : ℕ) (a : A) : gsmul (Int.negSucc n) a = -(gsmul ↑(n.succ) a)
 
 section AddGroup_lemmas
 
@@ -232,7 +245,7 @@ theorem add_neg_self (a : A) : a + -a = 0 := add_right_neg a
 by rw [add_assoc, add_right_neg, add_zero]
 
 instance (A : Type u) [AddGroup A] : IsAddRightCancel A where
-  add_right_cancel a b c h := by 
+  add_right_cancel a b c h := by
   rw [← add_neg_cancel_right b a, h, add_neg_cancel_right]
 
 instance (A : Type u) [AddGroup A] : IsAddLeftCancel A where
@@ -357,17 +370,27 @@ instance (M : Type u) [CommMonoid M] : CommSemigroup M where
 
 /-
 
+### Div inv monoids
+-/
+
+class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G :=
+(div := λ a b => a * b⁻¹)
+(div_eq_mul_inv : ∀ a b : G, a / b = a * b⁻¹)
+(gpow : ℤ → G → G := gpow_rec)
+(gpow_zero' : ∀ (a : G), gpow 0 a = 1)
+(gpow_succ' :
+  ∀ (n : ℕ) (a : G), gpow (Int.ofNat n.succ) a = a * gpow (Int.ofNat n) a)
+(gpow_neg' :
+  ∀ (n : ℕ) (a : G), gpow (Int.negSucc n) a = (gpow n.succ a) ⁻¹)
+
+/-
+
 ### Groups
 
 -/
 
-class Group (G : Type u) extends Monoid G, Inv G, Div G where
+class Group (G : Type u) extends DivInvMonoid G where
   mul_left_inv (a : G) : a⁻¹ * a = 1
-  div_eq_mul_inv (a b : G) : a / b = a * b⁻¹ 
-  gpow : ℤ → G → G := gpow_rec
-  gpow_zero' (a : G) : gpow 0 a = 1 -- try rfl
-  gpow_succ' (n : ℕ) (a : G) : gpow (Int.ofNat n.succ) a = a * gpow (Int.ofNat n) a 
-  gpow_neg' (n : ℕ) (a : G) : gpow (Int.negSucc n) a = (gpow ↑(n.succ) a)⁻¹
 
 section Group_lemmas
 

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -4,13 +4,12 @@ class MonoidWithZero (M₀ : Type u) extends Monoid M₀, Zero M₀ where
   zero_mul (a : M₀) : 0 * a = 0
   mul_zero (a : M₀) : a * 0 = 0
 
-class GroupWithZero (G₀ : Type u) extends MonoidWithZero G₀, Inv G₀, Div G₀ where
-  mul_left_inv (a : G₀) : a⁻¹ * a = 1
-  div_eq_mul_inv (a b : G₀) : a / b = a * b⁻¹ 
-  gpow : ℤ → G₀ → G₀ := gpow_rec
-  gpow_zero' (a : G₀) : gpow 0 a = 1 -- try rfl
-  gpow_succ' (n : ℕ) (a : G₀) : gpow (Int.ofNat n.succ) a = a * gpow (Int.ofNat n) a 
-  gpow_neg' (n : ℕ) (a : G₀) : gpow (Int.negSucc n) a = (gpow ↑(n.succ) a)⁻¹
+class GroupWithZero (G₀ : Type u) extends DivInvMonoid G₀, Zero G₀ where
   exists_pair_ne : ∃ (x y : G₀), x ≠ y
+  zero_mul (a : G₀) : 0 * a = 0
+  mul_zero (a : G₀) : a * 0 = 0
   inv_zero : (0 : G₀)⁻¹ = 0
-  mul_inv_cancel (a : G₀) : a ≠ 0 → a * a⁻¹ = 1
+  mul_inv_cancel (a : G₀) : a ≠ 0 → a * a⁻¹ = 1
+
+instance (G₀ : Type u) [h : GroupWithZero G₀] : MonoidWithZero G₀ :=
+{h with }