commutator_perm_le — Mathlib

English

The commutator of the full permutation group lies inside the alternating group.

Русский

Коммутатор полной группы перестановок лежит внутри чередующейся группы.

LaTeX

$$$commutator(Perm(\alpha)) \le Alt(\alpha)$$$

Lean4

theorem commutator_perm_le : commutator (Perm α) ≤ alternatingGroup α :=
  by
  simp only [commutator_eq_closure, closure_le, Set.subset_def, mem_commutatorSet_iff, SetLike.mem_coe,
    mem_alternatingGroup, forall_exists_index]
  rintro _ p q rfl
  simp [map_commutatorElement, commutatorElement_eq_one_iff_commute, Commute.all]

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