neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq

English

For f, p, x, v as above, (-1)^{p} • f(p.insertNth x v) = f(Matrix.vecCons x v).

Русский

Для тех же условий, (-1)^p • f(p.insertNth x v) = f(Matrix.vecCons x v).

LaTeX

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

Lean4

/-- Let `v` be an `(n + 1)`-tuple with two equal elements `v i = v j`, `i ≠ j`.
Let `w i` (resp., `w j`) be the vector `v` with `i`th (resp., `j`th) element removed.
Then `(-1) ^ i • f (w i) + (-1) ^ j • f (w j) = 0`.
This follows from the fact that these two vectors differ by a permutation of sign `(-1) ^ (i + j)`.

These are the only two nonzero terms in the proof of `map_eq_zero_of_eq`
in the definition of `AlternatingMap.alternatizeUncurryFin`. -/
theorem neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq (f : E [⋀^Fin n]→L[𝕜] F) {v : Fin (n + 1) → E}
    {i j : Fin (n + 1)} (hvij : v i = v j) (hij : i ≠ j) :
    (-1) ^ (i : ℕ) • f (i.removeNth v) + (-1) ^ (j : ℕ) • f (j.removeNth v) = 0 :=
  f.toAlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq hvij hij

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