Theorems · Theorem · group theory

alternatingGroup.normal_subgroup_eq_bot_or_eq_top_of_card_ne_eight

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

If α has at least 5 elements, but not 8, then the only nontrivial normal subgroup of alternatingGroup α is ⊤.

Defined in

Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeSubgroup.Normal