Prime_Group_has_no_Proper_Subgroups
Provedgroup-theoryprimeproofwikisubgroup
A group of prime order has no proper subgroups other than the trivial group and itself.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Prime_Group_has_no_Proper_Subgroups {G : Type _} [Group G] [Fintype G] {p : ℕ} (hp : Nat.Prime p) (hG : Fintype.card G = p) (H : Subgroup G) : H = ⊥ ∨ H = ⊤ := by sorrySource