neg_one_pow_smul_map_insertNth — Mathlib

English

For a continuous alternating map f, inserting x at position p in v yields the evaluated value at p.insertNth x v equal to (-1)^{p} times the value at Matrix.vecCons x v.

Русский

При вставке x на позицию p в векторе v выражение f(p.insertNth x v) равно (-1)^p умноженному на f(Matrix.vecCons x v).

LaTeX

$$$f(p.insertNth x v) = (-1)^{p} \\cdot f(Matrix.vecCons x v)$$$

Lean4

theorem neg_one_pow_smul_map_insertNth (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (p : Fin (n + 1)) (x : E) (v : Fin n → E) :
    (-1) ^ (p : ℕ) • f (p.insertNth x v) = f (Matrix.vecCons x v) :=
  f.toAlternatingMap.neg_one_pow_smul_map_insertNth p x v

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