mem_commutator_alternatingGroup — Mathlib

English

If g is a three-cycle in the alternating group on α, then g lies in the commutator group of alternatingGroup α.

Русский

Если g — трёхцикл в чередующейся группе на α, то g принадлежит коммутаторной подгруппе AlternatingGroup α.

LaTeX

$$$g IsThreeCycle\Rightarrow g \in commutator(AlternatingGroup(\alpha))$$$

Lean4

theorem mem_commutator_alternatingGroup : g ∈ commutator (alternatingGroup α) :=
  by
  rw [commutator_eq_closure]
  apply Subgroup.subset_closure
  exact hg.mem_commutatorSet_alternatingGroup h5

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