See also MulAut.conj and Quandle.conj.
We say that a is conjugate to b if for some unit c we have c * a * c⁻¹ = b.
c * a * c⁻¹ = b
The setoid of the relation IsConj iff there is a unit u such that u * x = y * u
u * x = y * u
The quotient type of conjugacy classes of a group.
The canonical quotient map from a monoid α into the ConjClasses of α
A MonoidHom maps conjugacy classes of one group to conjugacy classes of another.
The bijection between a CommGroup and its ConjClasses.
Given an element a, conjugatesOf a is the set of conjugates.
Given a conjugacy class a, carrier a is the set it represents.