val_conj_smul — Mathlib

English

For a normal subgroup H, the action of an element g ∈ G by conjugation on an element h ∈ H coincides with the inclusion of h into G and then acting by g: the inclusion respects the action, i.e., g•h (as an element of H) maps to g h g^{-1} in G.

Русский

Пусть H нормальна в G. Тогда действие сопряжением элемента g на h ∈ H согласуется с включением H в G: g•h в H соответствует g h g^{-1} в G.

LaTeX

$$$ (g \cdot h) = (g h g^{-1}) \text{ under the inclusion } H \hookrightarrow G. $$$

Lean4

theorem val_conj_smul {H : Subgroup G} [H.Normal] (g : ConjAct G) (h : H) : ↑(g • h) = g • (h : G) :=
  rfl

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