Theorems · Theorem · group theory

Sylow.exists_subgroup_card_pow_succ

∀ {G : Type u} [inst : Group G] [Finite G] {p n : ℕ} [hp : Fact (Nat.Prime p)],
  p ^ (n + 1) ∣ Nat.card G → ∀ {H : Subgroup G}, Nat.card ↥H = p ^ n → ∃ K, Nat.card ↥K = p ^ (n + 1) ∧ H ≤ K

If H is a subgroup of G of cardinality p ^ n, then H is contained in a subgroup of cardinality p ^ (n + 1) if p ^ (n + 1) divides the cardinality of G

Defined in

Mathlib.GroupTheory.Sylow

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupFiniteFact