smul_eq_of_normal — Mathlib

English

If P is normal in G, then for every g ∈ G, the Sylow subgroup P is invariant under conjugation by g: g · P = P.

Русский

Если P нормальна в G, то для каждого g ∈ G подгруппа P сохраняется при сопряжении: g · P = P.

LaTeX

$$$P \\trianglelefteq G \\Rightarrow g \\cdot P = P \\quad \\text{for all } g \\in G.$$$

Lean4

theorem smul_eq_of_normal {g : G} {P : Sylow p G} [h : P.Normal] : g • P = P := by
  simp only [smul_eq_iff_mem_normalizer, P.normalizer_eq_top, mem_top]

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