sign_prodExtendRight — Mathlib

English

Extending a permutation on a single coordinate by σ does not change the parity of the permutation.

Русский

Расширение перестановки по одной координате σ не меняет знак.

LaTeX

$$$\\operatorname{sign}(\\operatorname{prodExtendRight}(a,\\sigma))=\\operatorname{sign}(\\sigma)$$$

Lean4

@[simp]
theorem sign_prodExtendRight (a : α) (σ : Perm β) : sign (prodExtendRight a σ) = sign σ :=
  sign_bij (fun (ab : α × β) _ => ab.snd) (fun ⟨a', b⟩ hab _ => by simp [eq_of_prodExtendRight_ne hab])
    (fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ hab₁ hab₂ h => by
      simpa [eq_of_prodExtendRight_ne hab₁, eq_of_prodExtendRight_ne hab₂] using h)
    fun y hy => ⟨(a, y), by simpa, by simp⟩

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