Theorems · Theorem · group theory

Sylow.exists_subgroup_card_pow_prime

• #72 of the 100 theorems: Sylow’s Theorem
• 1000+ list: Sylow theorems

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

A generalisation of Sylow's first theorem. If p ^ n divides the cardinality of G, then there is a subgroup of cardinality p ^ n

Defined in

Mathlib.GroupTheory.Sylow

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupFiniteFact