Group Theory

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, 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