English
A subgroup of G with cardinality p^n, where n is the p-adic multiplicity of |G|, is a Sylow p-subgroup of G.
Русский
Подгруппа G размером p^n, где n — показатель степени p в порядке G, является подпогруппой Силова p в G.
LaTeX
$$$[Finite\\ G] \\Rightarrow \\exists H: Subgroup(G), \\text{card}(H) = p^{\\text{card}(G).factorization(p)} \\,\\Rightarrow \\, \\text{Sylow}_p(G) \\text{ contains } H$$$
Lean4
/-- A subgroup with cardinality `p ^ n` is a Sylow subgroup
where `n` is the multiplicity of `p` in the group order. -/
def ofCard [Finite G] {p : ℕ} [Fact p.Prime] (H : Subgroup G)
(card_eq : Nat.card H = p ^ (Nat.card G).factorization p) : Sylow p G :=
(IsPGroup.of_card card_eq).toSylow
(by
rw [← mul_dvd_mul_iff_left (Nat.card_pos (α := H)).ne', card_mul_index, card_eq, ← pow_succ]
exact Nat.pow_succ_factorization_not_dvd Nat.card_pos.ne' Fact.out)
