normal_of_normalizerCondition — Mathlib

English

If a group G satisfies NormalizerCondition, then every Sylow p-subgroup is normal in G.

Русский

Если группа G удовлетворяет условию NormalizerCondition, то любая Sylow p-подгруппа нормальна в G.

LaTeX

$$$\forall {G:\ TYPE u} [Group\ G], NormalizerCondition\ G\Rightarrow \forall {p}\ [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P:Sylow p G), P.Normal$$

Lean4

theorem normal_of_normalizerCondition (hnc : NormalizerCondition G) {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)]
    (P : Sylow p G) : P.Normal :=
  normalizer_eq_top_iff.mp <|
    normalizerCondition_iff_only_full_group_self_normalizing.mp hnc _ <| normalizer_normalizer _

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