Theorems · Theorem · group theory

Sylow.exists_subgroup_le_card_le

∀ {G : Type u} [inst : Group G] {k p : ℕ},
  Nat.Prime p →
    IsPGroup p G → ∀ {H : Subgroup G}, k ≤ Nat.card ↥H → k ≠ 0 → ∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'

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

Defined in

Mathlib.GroupTheory.Sylow

Cited by

1 results in Mathlib

Foundations

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

Assumes

Group