A group is a nonempty set \(G\) with a closed binary operation (\(\mu : G \times G \rightarrow G\)), satisfying the following group axioms:

• Associativity: \(\forall \, a, b, c \in G, ~ \mu (\mu (a, b), c) = \mu (a, \mu (b, c))\)

• Identity element: \(\mathbb {e}\in G\) where \(\forall \, a \in G, ~ \mu (a, \mathbb {e}) = \mu (\mathbb {e}, a) = a\)

• Inverses (\(\iota \)): \(\forall \, a \in G, ~ \mu (\iota (a), a) = \mathbb {e}\)

A magma is a set G with an operation \(\mu : G \rightarrow G \rightarrow G\)

A semigroup is a magma with the associative property: \(\forall a,~ b,~ c \in G, ~ \mu (\mu (a, b), c) = \mu (a,~ \mu (b, c))\)

A monoid is a semigroup with an identity \(\mathbb {e}\) where \(\forall a \in G, ~ \mu (a, \mathbb {e}) = \mu (\mathbb {e},~ a) = a\)

A commutative monoid is a monoid with the commutative property: \(\forall a,~ b \in G, ~ \mu (a, b) = \mu (b, a)\)

An abelian group is a group with the commutative property: \(\forall a,~ b \in G, ~ \mu (a,~ b) = \mu (b,~ a)\)

\((\mathbb {Z},~ +)\), the integers over addition, form a group, The identity of the group is \(0\), and the inverse of an element \(x \in \mathbb {Z}\) is \(-x\).

\(C_3\) is the group of rotational symmetries of an equilateral triangle with the group operation being the composition of symmetries. This is treated as an inductive type with three elements. The identity is a \( 0 ^{\circ } \) rotation, and the inverse of an \(x ^{\circ } \) rotation is a \((360 - x)^{\circ } \) rotation.

\(C_n\) is the generalization of \(C_3\), and is therefore the group of rotations of a regular n-gon. It uses mathlib’s Fin n type, and addition on that type. Since Fin allows modular arithmetic, rotations that are seperated by a multiple of \(360^{\circ }\) are treated as equal. Similarly to \(C_3\), the identity is a \(0^{\circ }\) rotation, and the inverse of an \(x ^{\circ }\) rotation is a \((360 - x)^{\circ }\) rotation.

\(D_n\) is the dihedral group of order \(2n\). This is the group of all symmetries of a regular n-gon. This includes n rotations and n reflections. It is represented by a pair of a boolean and an element of Fin n. The boolean represents whether the element is a rotation or not, and the element of Fin n represents how much the first vertex is rotated. The identity is a \(0^{\circ }\) rotation, the inverse of an \(x^{\circ }\) rotation is a \((360 - x)^{\circ }\) rotation, and any reflection is its own inverse.

\(S_n\), the symmetric group of order \(n!\), is the set of all permutations of \(n\) elements. It is represented as the set of all bijections from Fin n to Fin n, with function composition as the group operation. The identity is the identity function, and the inverse of a group element is its inverse function (which exists since all bijections are invertible).