alternatization_coe — Mathlib

English

The application of alternatization to m evaluated at v equals the sum over permutations of the signs times the domDomCongr action on v.

Русский

Применение alternatization к m в точке v равно сумме по перестановкам знаков, умноженных на действие domDomCongr σ на v.

LaTeX

$$$\\operatorname{alternatization}(m)(v) = \\sum_{\\sigma} \\operatorname{sign}(σ) · m \\mathrm{domDomCongr}(σ) v$$$

Lean4

theorem alternatization_coe (m : MultilinearMap R (fun _ : ι => M) N') :
    ↑(alternatization m) = (∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ :) :=
  coe_injective rfl

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