English
If P is a cyclic Sylow p-subgroup of G and p is the smallest prime dividing |G|, then ker(transferSylow) is a normal p-complement to P.
Русский
Если P — циклическая Sylow-p-подгруппа G и p — наименьшая простая, делящая |G|, то ядро переноса Sylow образует нормальный p-комплемент к P.
LaTeX
$$ker(\operatorname{transferSylow}(P,hP)).IsComplement' P$$
Lean4
/-- A cyclic Sylow subgroup for the smallest prime has a normal complement. -/
theorem isComplement' (hP : IsCyclic P) :
(MonoidHom.transferSylow P (hP.normalizer_le_centralizer hp)).ker.IsComplement' P :=
by
subst hp
by_cases hn : Nat.card G = 1
· have := (Nat.card_eq_one_iff_unique.mp hn).1
rw [Subsingleton.elim (MonoidHom.transferSylow P (hP.normalizer_le_centralizer rfl)).ker ⊥, Subsingleton.elim P.1 ⊤]
exact isComplement'_bot_top
have := Fact.mk (Nat.minFac_prime hn)
exact MonoidHom.ker_transferSylow_isComplement' P (hP.normalizer_le_centralizer rfl)
