Theorems · Theorem · group theory

alternatingGroup.normal_subgroup_eq_bot_or_eq_top

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  5 ≤ Nat.card α → ∀ {N : Subgroup ↥(alternatingGroup α)} [N.Normal], N = ⊥ ∨ N = ⊤

Defined in

Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Cited by

1 results in Mathlib

Foundations

Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeSubgroup.Normal