English
Let G be a group and p a prime. If the Sylow p-subgroup of G is unique (i.e. there is only one Sylow p-subgroup), then this Sylow p-subgroup is invariant under every automorphism of G; in particular it is a characteristic subgroup of G.
Русский
Пусть G — группа, p — простое число. Если единственный подгрупп Sylow p(G) существует, то она инвариантна относительно любых автоморфизмов группы G, то есть является характеристической подгруппой G.
LaTeX
$$$\forall G\,[Group\ G]\forall p\,[Prime\ p]\ [Subsingleton\ (Sylow\ p\ G)](P:\\ Sylow\ p\ G)\ \Rightarrow\ \forall \varphi\in Aut(G),\\ \varphi(P)=P$$$
Lean4
instance characteristic_of_subsingleton {p : ℕ} [Subsingleton (Sylow p G)] (P : Sylow p G) : P.Characteristic :=
by
refine Subgroup.characteristic_iff_map_eq.mpr fun ϕ ↦ ?_
have h := Subgroup.pointwise_smul_def (a := ϕ) (P : Subgroup G)
rwa [← pointwise_smul_def, Subsingleton.elim (ϕ • P) P, eq_comm] at h
