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.

@[reducible, inline]

abbrev 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) (inv_mul_cancel : ∀ (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 inv_mul_cancel = Group.mk inv_mul_cancel

@[reducible, inline]

abbrev 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) (inv_mul_cancel : ∀ (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 inv_mul_cancel = AddGroup.mk inv_mul_cancel

@[reducible, inline]

abbrev 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_inv_cancel : ∀ (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_inv_cancel = Group.mk ⋯

@[reducible, inline]

abbrev 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_inv_cancel : ∀ (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_inv_cancel = AddGroup.mk ⋯