alternatization_apply — Mathlib

English

The apply form of alternatization on m at v is the sum over σ of sign σ times the action on v by domDomCongr σ.

Русский

Форма применения alternatization к m на v равна сумме по σ от знака σ, умноженного на действие domDomCongr σ на v.

LaTeX

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

Lean4

theorem alternatization_apply (m : MultilinearMap R (fun _ : ι => M) N') (v : ι → M) :
    alternatization m v = ∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ v := by
  simp only [alternatization_def, smul_apply, sum_apply]

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