English
For a normal subgroup H ≤ G, the map sending g ∈ G to the inner automorphism of H given by h ↦ g h g^{-1} extends to a monoid homomorphism from G into the automorphism group of H, i.e., inner automorphisms of H induced by conjugation.
Русский
Пусть H нормальна в G. Отображение g ↦ (h ↦ g h g^{-1}) распростивается до моноидного гомоморфизма G → MulAut(H).
LaTeX
$$$\operatorname{conjNormal}_H: G \to^* \operatorname{MulAut}(H), \quad g \mapsto (h \mapsto g h g^{-1}).$$$
Lean4
/-- Group conjugation on a normal subgroup. Analogous to `MulAut.conj`. -/
def _root_.MulAut.conjNormal {H : Subgroup G} [H.Normal] : G →* MulAut H :=
(MulDistribMulAction.toMulAut (ConjAct G) H).comp toConjAct.toMonoidHom
