alternatization_apply_apply — Mathlib

English

Applying alternatization to a continuous multilinear map f and then evaluating at v ∈ M^{ι} yields the same as summing over permutations: alternatization f v = ∑_{σ} sign(σ) · f(v ∘ σ).

Русский

Применяя антисимметризацию к отображению f и затем вычисляя на v ∈ M^{ι}, получаем то же самое, что сумма по перестановкам: alternatization f v = ∑_{σ} sign(σ) · f(v ∘ σ).

LaTeX

$$$$ \\text{alternatization}(f)\\,v = \\sum_{σ \\in \\operatorname{Perm}(\\iota)} \\operatorname{sign}(σ) \\cdot f(v \\circ σ). $$$$

Lean4

theorem alternatization_apply_apply (v : ι → M) :
    alternatization f v = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • f (v ∘ σ) := by
  simp [alternatization, Function.comp_def]

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