map_vecCons_add — Mathlib

English

The alternating map is additive in the first vector argument built via vecCons: f(vecCons(x+y, m)) = f(vecCons(x, m)) + f(vecCons(y, m)).

Русский

Чередующееся отображение аддитивно по первому аргументу, построенному через vecCons: f(vecCons(x+y, m)) = f(vecCons(x, m)) + f(vecCons(y, m)).

LaTeX

$$$f(\\mathrm{Matrix}.vecCons(x+y, m)) = f(\\mathrm{Matrix}.vecCons(x, m)) + f(\\mathrm{Matrix}.vecCons(y, m))$$$

Lean4

/-- A version of `MultilinearMap.cons_add` for `AlternatingMap`. -/
theorem map_vecCons_add {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (x y : M) :
    f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m) :=
  f.toMultilinearMap.cons_add _ _ _

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