map_insertNth — Mathlib

English

If v has i and j equal, then the sum of two terms with i.removeNth and j.removeNth, weighted by (-1)^i and (-1)^j, is zero.

Русский

Если вектора имеют повторение, то соответствующая линейная комбинация нулевой чередующей карты равна нулю.

LaTeX

$$$(-1)^{i} \\cdot f(i.removeNth v) + (-1)^{j} \\cdot f(j.removeNth v) = 0$$$

Lean4

/-- If `f` is a continuous `(n + 1)`-multilinear alternating map, `x` is an element of the domain,
and `v` is an `n`-vector, then the value of `f` at `v` with `x` inserted at the `p`th place
equals `(-1) ^ p` times the value of `f` at `v` with `x` prepended. -/
theorem map_insertNth (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (p : Fin (n + 1)) (x : E) (v : Fin n → E) :
    f (p.insertNth x v) = (-1) ^ (p : ℕ) • f (Matrix.vecCons x v) :=
  f.toAlternatingMap.map_insertNth p x v

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