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.

theorem AddGroup.ofLeftAxioms.proof_3 {G : Type u_1} [Add G] [Zero G] : ∀ (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) : AddGroup G

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

• AddGroup.ofLeftAxioms assoc one_mul mul_left_inv = AddGroup.mk mul_left_inv

theorem AddGroup.ofLeftAxioms.proof_7 {G : Type u_1} [Add G] [Neg G] [Zero G] : ∀ (n : ℕ) (a : G), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) 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

theorem AddGroup.ofLeftAxioms.proof_2 {G : Type u_1} [Add G] [Zero G] : ∀ (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 (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) 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) : Group G

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

• Group.ofLeftAxioms assoc one_mul mul_left_inv = Group.mk mul_left_inv

theorem AddGroup.ofRightAxioms.proof_3 {G : Type u_1} [Add G] [Zero G] : ∀ (x : G), nsmulRec 0 x = nsmulRec 0 x

theorem AddGroup.ofRightAxioms.proof_4 {G : Type u_1} [Add G] [Zero G] : ∀ (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 (Int.negSucc n) a = zsmulRec (Int.negSucc n) 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) : AddGroup G

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

• AddGroup.ofRightAxioms assoc mul_one mul_right_inv = let_fun mul_left_inv := ⋯; AddGroup.mk mul_left_inv

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 (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) 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) : Group G

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

• Group.ofRightAxioms assoc mul_one mul_right_inv = let_fun mul_left_inv := ⋯; Group.mk mul_left_inv