Conjugation action of a group on itself #
This file defines the conjugation action of a group on itself. See also
the definition of conjugation as a homomorphism into the automorphism group.
Main definitions #
Implementation Notes #
The scalar action in defined in this file can also be written using
mul_aut.conj g • h. This
has the advantage of not using the type alias
conj_act, but the downside of this approach
is that some theorems about the group actions will not apply when since this
mul_aut.conj g • h describes an action of
mul_aut G on
G, and not an action of
As normal subgroups are closed under conjugation, they inherit the conjugation action of the underlying group.