Composition_Series_of_Group_of_Prime_Power_Order_v2
Provedcomposition-seriesgroup-theoryp-groupproofwiki
A group of prime power order p^n has a composition series of length n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Composition_Series_of_Group_of_Prime_Power_Order_v2 {G : Type _} [Group G] [Fintype G] {p : ℕ} {n : ℕ} (hp : Nat.Prime p) (hn : 1 ≤ n) (hG : Fintype.card G = p ^ n) : ∃ (f : Fin (n + 1) → Subgroup G), f ⟨n, Nat.lt.base n⟩ = ⊤ ∧ f ⟨0, Nat.zero_lt_succ n⟩ = ⊥ := by sorrySource