commutator_perm_eq — Mathlib

English

The commutator subgroup of the full symmetric group on α equals the alternating group on α (for |α| ≥ 5).

Русский

Коммутаторная подгруппа полной группы перестановок над α равна чередующейся группе над α (при |α| ≥ 5).

LaTeX

$$$commutator\left(Perm(\alpha)\right) = Alt(\alpha)\quad\text{for } |\alpha| \ge 5$$$

Lean4

/-- The commutator subgroup of the permutation group is the alternating group -/
theorem commutator_perm_eq (h5 : 5 ≤ Fintype.card α) : commutator (Perm α) = alternatingGroup α :=
  by
  apply le_antisymm alternatingGroup.commutator_perm_le
  rw [← commutator_alternatingGroup_eq_self h5]
  exact commutator_mono le_top le_top

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