alternatization_def — Mathlib

English

The alternating map obtained from a multilinear map via alternatization coincides with the corresponding AddMonoidHom coercion of the same map’s alternatization.

Русский

Чередующаяся карта, полученная через alternatization, совпадает с сопоставлением через коэрцию AddMonoidHom для той же карты.

LaTeX

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

Lean4

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

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