alternatizeUncurryFin_curryLeft — Mathlib

English

Explicit evaluation formula for alternatizeUncurryFin.

Русский

Явная формула вычисления alternatizeUncurryFin.

LaTeX

$$$\\text{alternatizeUncurryFin} f\, v = \\sum_{i : Fin (n+1)} (-1)^{i} \\cdot f (v_i) (\\operatorname{removeNth} i\, v)$$$

Lean4

@[simp]
theorem alternatizeUncurryFin_curryLeft (f : E [⋀^Fin (n + 1)]→L[𝕜] F) :
    alternatizeUncurryFin (curryLeft f) = (n + 1) • f := by
  ext v
  simp [alternatizeUncurryFin_apply, ← map_insertNth]

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