kleinFour — Mathlib

English

The subgroup of Alt α generated by double transpositions, i.e., cycle type (2,2).

Русский

Подгруппа Alt α, порождаемая двойными перестановками (типа цикла 2,2).

LaTeX

$$def kleinFour : Subgroup (alternatingGroup α) := Subgroup.closure {g : alternatingGroup α | (g : Equiv.Perm α).cycleType = { 2, 2 }}$$

Lean4

/-- The subgroup of `alternatingGroup α` generated by permutations of cycle type (2, 2).

When `Nat.card α = 4`, it will effectively be of Klein Four type. -/
def kleinFour : Subgroup (alternatingGroup α) :=
  Subgroup.closure {g : alternatingGroup α | (g : Equiv.Perm α).cycleType = { 2, 2 }}

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