Documentation

Mathlib.Algebra.Group.MinimalAxioms

Minimal Axioms for a Group #

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

Main Definitions #

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) :

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 (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) :

    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
      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) :

      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 (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) :

        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