English
A normal cyclic Sylow p-subgroup P is either contained in the center of the group or contained in the commutator subgroup.
Русский
Нормальная циклическая сигма-п-подгруппа P либо входит в центр группы, либо входит в коммутатор группы.
LaTeX
$$$P.normalizer \\le C_G(P) \\ \\lor\\ P \\le [G,G]$$$
Lean4
/-- A normal cyclic Sylow subgroup is either central or contained in the commutator subgroup. -/
theorem le_center_or_le_commutator [P.Normal] : P ≤ Subgroup.center G ∨ P ≤ commutator G :=
by
obtain ⟨K, hK⟩ := Subgroup.exists_left_complement'_of_coprime P.card_coprime_index
refine (commutator_eq_bot_or_commutator_eq_self P hK).imp (fun h ↦ ?_) (fun h ↦ ?_)
· replace h := sup_le (Subgroup.commutator_eq_bot_iff_le_centralizer.mp h) P.le_centralizer
rwa [hK.sup_eq_top, top_le_iff, Subgroup.centralizer_eq_top_iff_subset] at h
· rw [← h, commutator_def]
exact Subgroup.commutator_mono le_top le_top
