sign_prodCongrLeft — Mathlib

English

The sign of the left-congruence permutation factors as the product of the signs of the factors.

Русский

Знак левого конгруэнтного смешения равен произведению знаков факторов.

LaTeX

$$$\\operatorname{sign}(\\operatorname{prodCongrLeft}(\\sigma)) = \\prod k\\; \\operatorname{sign}(\\sigma(k))$$$

Lean4

theorem sign_prodCongrLeft (σ : α → Perm β) : sign (prodCongrLeft σ) = ∏ k, sign (σ k) :=
  by
  refine (sign_eq_sign_of_equiv _ _ (prodComm β α) ?_).trans (sign_prodCongrRight σ)
  rintro ⟨b, α⟩
  rfl

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