See also mul_aut.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 is_conj 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 conj_classes of α
A monoid_hom maps conjugacy classes of one group to conjugacy classes of another.
The bijection between a comm_group and its conj_classes.
Given an element a, conjugates a is the set of conjugates.
Given a conjugacy class a, carrier a is the set it represents.