English
A variant of insertNth additivity for the case with symmetric structure; the equality expresses additivity after inserting sums.
Русский
Вариант аддитивности insertNth для симметричной структуры; равенство выражает аддитивность после вставки суммы.
LaTeX
$$$ f(p.insertNth (instHAdd.hAdd x y) m) = instHAdd.hAdd (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 `cons`, one can express directly the multiplicativity
of a multilinear map along the first variable. -/
theorem snoc_smul (f : MultilinearMap R M M₂) (m : ∀ i : Fin n, M (castSucc i)) (c : R) (x : M (last n)) :
f (snoc m (c • x)) = c • f (snoc m x) := by
simp_rw [← update_snoc_last x m (c • x), f.map_update_smul, update_snoc_last]
