Burnside p^a q^b theorem

finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow

Submitter: Kim Morrison.

Notes: Burnside's theorem that a finite group of order p^a q^b is solvable.

Source: Classical theorem in finite group theory.

Informal solution: Use character theory and induction on the group order to prove solvability.

theorem declaration uses `sorry`finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow {G : Type*} [Group G] [Fintype G]
    {p q a b : ℕ}
    (hp : Nat.Prime p)
    (hq : Nat.Prime q)
    (hpq : p ≠ q)
    (hcard : Fintype.card G = p ^ a * q ^ b) :
    IsSolvable G := byG:Type u_1inst✝¹:Group Ginst✝:Fintype Gp:ℕq:ℕa:ℕb:ℕhp:Nat.Prime phq:Nat.Prime qhpq:p ≠ qhcard:Fintype.card G = p ^ a * q ^ b⊢ IsSolvable G
  sorryAll goals completed! 🐙

Solved by

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 18, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026

• @rishistyping with Stealth Model on May 22, 2026