alternatizeUncurryFin_apply — Mathlib

English

The applying rule for alternatizeUncurryFin is exactly the sum formula: alternatizeUncurryFin f v = ∑ i : Fin(n+1), (-1)^{i} • f (v_i) (removeNth i v).

Русский

Правило применения alternatizeUncurryFin записывается как сумма: alternatizeUncurryFin f v = ∑ i: Fin(n+1), (-1)^{i} • f (v_i) (removeNth i v).

LaTeX

$$$ alternatizeUncurryFin f v = \sum_{i \in \mathrm{Fin}(n+1)} (-1)^{i} \cdot f(v_i) (\mathrm{removeNth}\ i\ v)$$$

Lean4

theorem alternatizeUncurryFin_apply (f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v : Fin (n + 1) → M) :
    alternatizeUncurryFin f v = ∑ i : Fin (n + 1), (-1) ^ (i : ℕ) • f (v i) (removeNth i v) := by
  simp [alternatizeUncurryFin]

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