English
If you insert into a vector at the N-th position and add two elements, the map value equals the sum of the maps with each element inserted separately.
Русский
Если вставить в вектор на N-ой позиции и сложить два элемента, значение отображения равно сумме значений отображения для каждого вставленного элемента по отдельности.
LaTeX
$$$ f(p.insertNth (x+y) m) = f(p.insertNth x m) + f(p.insertNth 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 `snoc`, one can express directly the additivity of a
multilinear map along the first variable. -/
theorem snoc_add (f : MultilinearMap R M M₂) (m : ∀ i : Fin n, M (castSucc i)) (x y : M (last n)) :
f (snoc m (x + y)) = f (snoc m x) + f (snoc m y) := by
simp_rw [← update_snoc_last x m (x + y), f.map_update_add, update_snoc_last]
