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.
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
Instances For
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
Instances For
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 ⋯
Instances For
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 ⋯