conjAct — Mathlib

English

E acts on N by conjugation; the action is by automorphisms of N.

Русский

E действует на N по конъюгированию; действие задаёт автоморфизмы группы N.

LaTeX

$$$\\text{conjAct} : E \\rightarrow^* \\mathrm{MulAut}(N)$$$

Lean4

/-- `E` acts on `N` by conjugation. -/
noncomputable def conjAct : E →* MulAut N
    where
  toFun
    e :=
    (MonoidHom.ofInjective S.inl_injective).trans <|
      (MulAut.conjNormal e).trans (MonoidHom.ofInjective S.inl_injective).symm
  map_one' := by
    ext _
    simp only [map_one, MulEquiv.trans_apply, MulAut.one_apply, MulEquiv.symm_apply_apply]
  map_mul' _
    _ := by
    ext _
    simp only [map_mul, MulEquiv.trans_apply, MulAut.mul_apply, MulEquiv.apply_symm_apply]

Похожие утверждения