English
The cardinality of a Sylow p-subgroup equals p^n where n is the p-adic multiplicity of |G|.
Русский
Кардинальность Sylow p-подгруппы равна p^n, где n — показатель разложения |G| на p-части.
LaTeX
$$card P = p^{Nat.factorization (card G) p}$$
Lean4
/-- The cardinality of a Sylow subgroup is `p ^ n`
where `n` is the multiplicity of `p` in the group order. -/
theorem card_eq_multiplicity [Finite G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G) :
Nat.card P = p ^ Nat.factorization (Nat.card G) p :=
by
obtain ⟨n, heq : Nat.card P = _⟩ := IsPGroup.iff_card.mp P.isPGroup'
refine Nat.dvd_antisymm ?_ (P.pow_dvd_card_of_pow_dvd_card (Nat.ordProj_dvd _ p))
rw [heq, ← hp.out.pow_dvd_iff_dvd_ordProj (show Nat.card G ≠ 0 from Nat.card_pos.ne'), ← heq]
exact P.1.card_subgroup_dvd_card
