normal_of_normalizer_normal — Mathlib

English

If the normalizer of a Sylow p-subgroup is a normal subgroup of G, then the Sylow p-subgroup is normal in G.

Русский

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

LaTeX

$$$\forall {G:\ TYPE u} [Group\ G] {p: \mathbb{N}} [Fact p.Prime] [Finite (Sylow p G)] (P: Sylow p G)\ (P.normalizer.N ormal)\Rightarrow P.Normal$$

Lean4

theorem normal_of_normalizer_normal {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
    (hn : P.normalizer.Normal) : P.Normal := by
  rw [← normalizer_eq_top_iff, ← normalizer_sup_eq_top' P le_normalizer, sup_idem]

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