sign_prod_list_swap — Mathlib

English

For a list l of permutations, if each element is a swap, then the sign of the product equals (-1)^{length(l)}.

Русский

Для списка перестановок, состоящего из свапов, знак произведения равен (-1)^{длина списка}.

LaTeX

$$$\forall l:\text{List}(\mathrm{Perm}(\alpha)),\ \big(\forall g\in l,\ g\text{ is a swap}\big) \to \mathrm{sign}(\prod l) = (-1)^{|l|}$$$

Lean4

theorem sign_prod_list_swap {l : List (Perm α)} (hl : ∀ g ∈ l, IsSwap g) : sign l.prod = (-1) ^ l.length :=
  by
  have h₁ : l.map sign = List.replicate l.length (-1) :=
    List.eq_replicate_iff.2
      ⟨by simp, fun u hu =>
        let ⟨g, hg⟩ := List.mem_map.1 hu
        hg.2 ▸ (hl _ hg.1).sign_eq⟩
  rw [← List.prod_replicate, ← h₁, List.prod_hom _ (@sign α _ _)]

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