mem_commutatorSet_alternatingGroup

English

The commutator subgroup of the full permutation group is contained in the alternating group.

Русский

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

LaTeX

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

Lean4

theorem mem_commutatorSet_alternatingGroup : g ∈ commutatorSet (alternatingGroup α) :=
  by
  apply mem_commutatorSet_of_isConj_sq
  apply alternatingGroup.isThreeCycle_isConj h5 hg
  simpa [sq] using hg.isThreeCycle_sq

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