normal_of_subsingleton — Mathlib

English

If there is a unique Sylow p-subgroup of G, then that Sylow p-subgroup is normal in G.

Русский

Если существует единственная подгруппа Sylow p(G), то она нормальна в G.

LaTeX

$$$\forall {G:\ TYPE u} [Group\ G] {p: \mathbb{N}} [Subsingleton (Sylow\ p\ G)] (P:\\ Sylow\ p\ G), P\ Normal$$

Lean4

theorem normal_of_subsingleton {p : ℕ} [Subsingleton (Sylow p G)] (P : Sylow p G) : P.Normal :=
  Subgroup.normal_of_characteristic _

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