Prime_Group_is_Simple_v2
Provedgroup-theoryprimeproofwikisimple-group
Groups of prime order are simple: every normal subgroup is trivial or the whole group.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Prime_Group_is_Simple_v2 {G : Type _} [Group G] [Fintype G] {p : ℕ} (hp : Nat.Prime p) (hG : Fintype.card G = p) (N : Subgroup G) [N.Normal] : N = ⊥ ∨ N = ⊤ := by sorrySource