# Minimal Axioms for a Group #

This file defines constructors to define a group structure on a Type, while proving only three equalities.

## Main Definitions #

• Group.ofLeftAxioms: Define a group structure on a Type by proving ∀ a, 1 * a = a and ∀ a, a⁻¹ * a = 1 and associativity.
• Group.ofRightAxioms: Define a group structure on a Type by proving ∀ a, a * 1 = a and ∀ a, a * a⁻¹ = 1 and associativity.
∀ (n : ) (x : G), nsmulRec (n + 1) x = nsmulRec (n + 1) x
@[reducible]
def AddGroup.ofLeftAxioms {G : Type u} [Add G] [Neg G] [Zero G] (assoc : ∀ (a b c : G), a + b + c = a + (b + c)) (one_mul : ∀ (a : G), 0 + a = a) (mul_left_inv : ∀ (a : G), -a + a = 0) :

Define an AddGroup structure on a Type by proving ∀ a, 0 + a = a and ∀ a, -a + a = 0. Note that this uses the default definitions for nsmul, zsmul and sub. See note [reducible non-instances].

Equations
Instances For
theorem AddGroup.ofLeftAxioms.proof_7 {G : Type u_1} [Add G] [Neg G] [Zero G] :
∀ (n : ) (a : G), zsmulRec () a = zsmulRec () a
theorem AddGroup.ofLeftAxioms.proof_1 {G : Type u_1} [Add G] [Neg G] [Zero G] (assoc : ∀ (a b c : G), a + b + c = a + (b + c)) (one_mul : ∀ (a : G), 0 + a = a) (mul_left_inv : ∀ (a : G), -a + a = 0) (a : G) :
a + 0 = a
theorem AddGroup.ofLeftAxioms.proof_4 {G : Type u_1} [Add G] [Neg G] [Zero G] (assoc : ∀ (a b c : G), a + b + c = a + (b + c)) (one_mul : ∀ (a : G), 0 + a = a) (mul_left_inv : ∀ (a : G), -a + a = 0) :
∀ (a b : G), a - b = a - b
theorem AddGroup.ofLeftAxioms.proof_5 {G : Type u_1} [Add G] [Neg G] [Zero G] :
∀ (a : G), zsmulRec 0 a = zsmulRec 0 a
∀ (x : G), nsmulRec 0 x = nsmulRec 0 x
theorem AddGroup.ofLeftAxioms.proof_6 {G : Type u_1} [Add G] [Neg G] [Zero G] :
∀ (n : ) (a : G), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a
@[reducible]
def Group.ofLeftAxioms {G : Type u} [Mul G] [Inv G] [One G] (assoc : ∀ (a b c : G), a * b * c = a * (b * c)) (one_mul : ∀ (a : G), 1 * a = a) (mul_left_inv : ∀ (a : G), a⁻¹ * a = 1) :

Define a Group structure on a Type by proving ∀ a, 1 * a = a and ∀ a, a⁻¹ * a = 1. Note that this uses the default definitions for npow, zpow and div. See note [reducible non-instances].

Equations
Instances For
∀ (x : G), nsmulRec 0 x = nsmulRec 0 x
∀ (n : ) (x : G), nsmulRec (n + 1) x = nsmulRec (n + 1) x
theorem AddGroup.ofRightAxioms.proof_8 {G : Type u_1} [Add G] [Neg G] [Zero G] :
∀ (n : ) (a : G), zsmulRec () a = zsmulRec () a
theorem AddGroup.ofRightAxioms.proof_1 {G : Type u_1} [Add G] [Neg G] [Zero G] (assoc : ∀ (a b c : G), a + b + c = a + (b + c)) (mul_one : ∀ (a : G), a + 0 = a) (mul_right_inv : ∀ (a : G), a + -a = 0) (a : G) :
-a + a = 0
theorem AddGroup.ofRightAxioms.proof_5 {G : Type u_1} [Add G] [Neg G] [Zero G] (assoc : ∀ (a b c : G), a + b + c = a + (b + c)) (mul_one : ∀ (a : G), a + 0 = a) (mul_right_inv : ∀ (a : G), a + -a = 0) (mul_left_inv : ∀ (a : G), -a + a = 0) :
∀ (a b : G), a - b = a - b
@[reducible]
def AddGroup.ofRightAxioms {G : Type u} [Add G] [Neg G] [Zero G] (assoc : ∀ (a b c : G), a + b + c = a + (b + c)) (mul_one : ∀ (a : G), a + 0 = a) (mul_right_inv : ∀ (a : G), a + -a = 0) :

Define an AddGroup structure on a Type by proving ∀ a, a + 0 = a and ∀ a, a + -a = 0. Note that this uses the default definitions for nsmul, zsmul and sub. See note [reducible non-instances].

Equations
Instances For
theorem AddGroup.ofRightAxioms.proof_6 {G : Type u_1} [Add G] [Neg G] [Zero G] :
∀ (a : G), zsmulRec 0 a = zsmulRec 0 a
theorem AddGroup.ofRightAxioms.proof_2 {G : Type u_1} [Add G] [Neg G] [Zero G] (assoc : ∀ (a b c : G), a + b + c = a + (b + c)) (mul_one : ∀ (a : G), a + 0 = a) (mul_right_inv : ∀ (a : G), a + -a = 0) (mul_left_inv : ∀ (a : G), -a + a = 0) (a : G) :
0 + a = a
theorem AddGroup.ofRightAxioms.proof_7 {G : Type u_1} [Add G] [Neg G] [Zero G] :
∀ (n : ) (a : G), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a
@[reducible]
def Group.ofRightAxioms {G : Type u} [Mul G] [Inv G] [One G] (assoc : ∀ (a b c : G), a * b * c = a * (b * c)) (mul_one : ∀ (a : G), a * 1 = a) (mul_right_inv : ∀ (a : G), a * a⁻¹ = 1) :

Define a Group structure on a Type by proving ∀ a, a * 1 = a and ∀ a, a * a⁻¹ = 1. Note that this uses the default definitions for npow, zpow and div. See note [reducible non-instances].

Equations
Instances For