Group Theory
============

<!--
SPDX-FileCopyrightText: The authors of this work have dedicated it to the public domain.
For more information, please refer to <https://unlicense.org/>
SPDX-License-Identifier: Unlicense
-->

Equational axioms for Group theory.

Various other documents require this document.

Note, we could define only `#id-right` and `#inv-right` as axioms,
and derive `#id-left` and `#inv-left` from them; see
[Right Inverse for All is Left Inverse](semigroup-right-inverse-is-left.eqthy.md), for instance.
But for brevity we'll just define them as axioms here.

    axiom (#id-right)   mul(A, e) = A
    axiom (#id-left)    mul(e, A) = A
    axiom (#assoc)      mul(A, mul(B, C)) = mul(mul(A, B), C)
    axiom (#inv-right)  mul(A, inv(A)) = e
    axiom (#inv-left)   mul(inv(A), A) = e