index_eq_two — Mathlib

English

The Klein four subgroup equals the commutator subgroup of the alternating group.

Русский

Подгруппа Klein Four равна коммутаторной подгруппе чередующейся группы.

LaTeX

$$$\mathrm{kleinFour}(\alpha) = \mathrm{commutator}(\mathrm{alternatingGroup}(\alpha))$$$

Lean4

@[simp]
theorem index_eq_two [Nontrivial α] : (alternatingGroup α).index = 2 :=
  by
  rw [alternatingGroup, index_ker, MonoidHom.range_eq_top.mpr (sign_surjective α)]
  simp_rw [mem_top, Nat.card_eq_fintype_card, card_subtype_true, card_units_int]

Похожие утверждения