English
If a finite group is the direct product of its Sylow subgroups, it is nilpotent.
Русский
Если конечная группа является прямым произведением своих Сило-подгрупп, она нильпотентна.
LaTeX
$$$\\operatorname{IsNilpotent}(G) \\iff \\exists \\text{ Sylow decomposition } G = \\prod_p P_p$$$
Lean4
/-- If a finite group is the direct product of its Sylow groups, it is nilpotent -/
theorem isNilpotent_of_product_of_sylow_group
(e : (∀ p : (Nat.card G).primeFactors, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G) : IsNilpotent G := by
classical
let ps := (Nat.card G).primeFactors
have : ∀ (p : ps) (P : Sylow p G), IsNilpotent (↑P : Subgroup G) :=
by
intro p P
haveI : Fact (Nat.Prime ↑p) := Fact.mk <| Nat.prime_of_mem_primeFactors p.2
exact P.isPGroup'.isNilpotent
exact nilpotent_of_mulEquiv e
