Prime_Power_Group_has_Non_Trivial_Proper_Normal_Subgroup
Provedgroup-theorynormal-subgroupp-groupproofwiki
If G is a group of order p^n with n > 1, then G has a proper non-trivial normal subgroup.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Prime_Power_Group_has_Non_Trivial_Proper_Normal_Subgroup {G : Type _} [Group G] [Fintype G] {p : ℕ} {n : ℕ} (hp : Nat.Prime p) (hn : 1 < n) (hG : Fintype.card G = p ^ n) : ∃ N : Subgroup G, N.Normal ∧ N ≠ ⊥ ∧ N ≠ ⊤ := by sorrySource