prod_list_swap_mem_alternatingGroup_iff_even_length

English

As a set inside Alt(α), KleinFour α equals {1} ∪ { g ∈ Alt(α) | (g : Perm α).cycleType = {2,2} } (set description).

Русский

Как множество внутри Alt(α), KleinFour(α) равняется {1} ∪ { g ∈ Alt(α) | (g : Perm α).cycleType = {2,2} } (описание множества).

LaTeX

$$(\mathrm{kleinFour}(\alpha) : Set(\mathrm{alternatingGroup}(\alpha))) = { 1 } ∪ { g : \mathrm{alternatingGroup}(\alpha) | (g : \mathrm{Perm}(\alpha)).cycleType = { 2, 2 } }$$

Lean4

theorem prod_list_swap_mem_alternatingGroup_iff_even_length {l : List (Perm α)} (hl : ∀ g ∈ l, IsSwap g) :
    l.prod ∈ alternatingGroup α ↔ Even l.length :=
  by
  rw [mem_alternatingGroup, sign_prod_list_swap hl, neg_one_pow_eq_one_iff_even]
  decide

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