characteristic_of_normal — Mathlib

English

In a finite group, if a Sylow p-subgroup is normal, then it is characteristic in the ambient group.

Русский

В конечной группе, если подгруппа Sylow p является нормальной, то она характеристическая в этой группе.

LaTeX

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

Lean4

theorem characteristic_of_normal {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) (h : P.Normal) :
    P.Characteristic := by
  have _ := unique_of_normal P h
  exact characteristic_of_subsingleton _

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