domDomCongr_perm — Mathlib

English

For a finite index set ι, permuting the arguments by any σ ∈ Perm ι changes an alternating map by the sign of σ; more precisely g.domDomCongr σ = sign(σ) · g.

Русский

Для конечного множества индексов ι перестановка аргументов действием σ из Perm ι изменяет чередующееся отображение на знак перестановки; точнее g.domDomCongr σ = sign(σ) · g.

LaTeX

$$$g \\;\\text{is mapped to} \\; \\operatorname{sign}(\\sigma)\\,g$ under domDomCongr σ.$$

Lean4

theorem domDomCongr_perm [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) : g.domDomCongr σ = Equiv.Perm.sign σ • g :=
  AlternatingMap.ext fun v => g.map_perm v σ

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