Theorems · Theorem · group theory

Sylow.exists_subgroup_le_card_pow_prime_of_le_card

∀ {G : Type u} [inst : Group G] {n p : ℕ},
  Nat.Prime p → IsPGroup p G → ∀ {H : Subgroup G}, p ^ n ≤ Nat.card ↥H → ∃ H' ≤ H, Nat.card ↥H' = p ^ n

A special case of Sylow's first theorem. If G is a p-group and H a subgroup of size at least p ^ n then there is a subgroup of H of cardinality p ^ n.

Defined in

Mathlib.GroupTheory.Sylow

Cited by

1 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group