English
If G is finite, then the Frattini subgroup frattini(G) is nilpotent.
Русский
Если G конечна, то Frattini(G) нильпотентна.
LaTeX
$$$[Finite\\ G] \\Rightarrow Group.IsNilpotent(\\operatorname{frattini}(G))$$$
Lean4
/-- When `G` is finite, the Frattini subgroup is nilpotent. -/
theorem frattini_nilpotent [Finite G] : Group.IsNilpotent (frattini G) := by
-- We use the characterisation of nilpotency in terms of all Sylow subgroups being normal.
have q := (isNilpotent_of_finite_tfae (G := frattini G)).out 0 3
rw [q]; clear q
intro p p_prime P
have frattini_argument := Sylow.normalizer_sup_eq_top P
have normalizer_P := frattini_nongenerating frattini_argument
have P_normal_in_G : (map (frattini G).subtype P).Normal := normalizer_eq_top_iff.mp normalizer_P
exact P_normal_in_G.of_map_subtype
