conjMulDistribMulAction — Mathlib

English

If H is a normal subgroup of G, then the action of the conjugation action (ConjAct G) on H is a MulDistribMulAction; equivalently, g • (h1 h2) = (g • h1)(g • h2).

Русский

Если H — нормальная подгруппа G, то на H действует действие сопряжения; т. е. (g)•(h1 h2) = (g)•h1 · (g)•h2.

LaTeX

$$$ g \cdot (h_1 h_2) = (g \cdot h_1)(g \cdot h_2), \quad (g \cdot h_i) = g h_i g^{-1}. $$$

Lean4

instance conjMulDistribMulAction {H : Subgroup G} [H.Normal] : MulDistribMulAction (ConjAct G) H :=
  Subtype.coe_injective.mulDistribMulAction H.subtype Subgroup.val_conj_smul

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