English
If every maximal subgroup of a finite group is normal, then every Sylow subgroup is normal.
Русский
Если в конечной группе каждая максимальная подгруппа нормальна, то каждая подгруппа Sylow нормальна.
LaTeX
$$$[Finite\ G]\ (\forall H\ Subgroup\ G, IsCoatom\ H\rightarrow H.Normal)\Rightarrow \forall {p}\ [Fact p.Prime]\ [Finite (Sylow p G)]\ (P:\ Sylow p G), P.Normal$$
Lean4
theorem normal_of_all_max_subgroups_normal [Finite G] (hnc : ∀ H : Subgroup G, IsCoatom H → H.Normal) {p : ℕ}
[Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) : P.Normal :=
normalizer_eq_top_iff.mp
(by
rcases eq_top_or_exists_le_coatom P.normalizer with (heq | ⟨K, hK, hNK⟩)
· exact heq
· haveI := hnc _ hK
have hPK : P ≤ K := le_trans le_normalizer hNK
refine (hK.1 ?_).elim
rw [← sup_of_le_right hNK, P.normalizer_sup_eq_top' hPK])
