Group


Axioms

        assoc: ?a * ?b * ?c = ?a * (?b * ?c)
 left_neutral: 1 * ?a = ?a
right_neutral: ?a * 1 = ?a
 left_inverse: inverse ?a * ?a = 1
right_inverse: ?a * inverse ?a = 1
THEOREM   

The group product is right-cancellative.

$$\forall a,b,c \in S : ba = ca \Rightarrow b = c$$

Proof available

THEOREM   

The group product is left-cancellative.

$$\forall a,b,c \in S : ab = ac \Rightarrow b = c$$

Proof available

THEOREM   

The group product is cancellative.

Proof available

THEOREM    \(\left(g^{-1}\right)^{-1} = g\)

Proof available

THEOREM   

Group has Latin square property.

Proof available