English
Along Fin (n+1) index, additivity in the first variable translates into a corresponding additivity after consing coordinates; f(cons (x+y) m) = f(cons x m) + f(cons y m).
Русский
В случае индексов Fin (n+1) сложение в первой переменной соответствует сложению после применения констер-конструкции: f(cons (x+y) m) = f(cons x m) + f(cons y m).
LaTeX
$$$ f(\text{cons}(x+y) m) = f(\text{cons}(x) m) + f(\text{cons}(y) m) $$$
Lean4
/-- In the specific case of multilinear maps on spaces indexed by `Fin (n+1)`, where one can build
an element of `∀ (i : Fin (n+1)), M i` using `cons`, one can express directly the additivity of a
multilinear map along the first variable. -/
theorem cons_add (f : MultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (x y : M 0) :
f (cons (x + y) m) = f (cons x m) + f (cons y m) := by
simp_rw [← update_cons_zero x m (x + y), f.map_update_add, update_cons_zero]
