# 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].

## 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].

## 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].

## 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].