English
The additivity result with scalars transfers under the cons construction: f(cons (c•x) m) = c•f(cons x m).
Русский
Результат аддитивности при скаляре переносится через конструкцию cons: f(cons (c•x) m) = c•f(cons x m).
LaTeX
$$$ f(\text{cons}(c \cdot x) m) = c \cdot f(\text{cons} x 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 cons_smul (f : MultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (c : R) (x : M 0) :
f (cons (c • x) m) = c • f (cons x m) := by
simp_rw [← update_cons_zero x m (c • x), f.map_update_smul, update_cons_zero]
