exists_subgroup_card_pow_prime — Mathlib

English

If G is a finite group and p^n divides |G|, there exists a Sylow p-subgroup of cardinality p^n.

Русский

Если G — конечная группа и p^n делит |G|, существует подгруппа Шилова p-порядка p^n.

LaTeX

$$∃ H: Subgroup G, card H = p^n$$

Lean4

/-- A generalisation of **Sylow's first theorem**. If `p ^ n` divides
  the cardinality of `G`, then there is a subgroup of cardinality `p ^ n` -/
theorem exists_subgroup_card_pow_prime [Finite G] (p : ℕ) {n : ℕ} [Fact p.Prime] (hdvd : p ^ n ∣ Nat.card G) :
    ∃ K : Subgroup G, Nat.card K = p ^ n :=
  let ⟨K, hK⟩ := exists_subgroup_card_pow_prime_le p hdvd ⊥ (by rw [card_bot, pow_zero]) n.zero_le
  ⟨K, hK.1⟩

Похожие утверждения