English
The vecCons construction is linear in the scalar factor: f(vecCons(c•x, m)) = c • f(vecCons(x, m)).
Русский
Конструкция vecCons линейна по скаляру: f(vecCons(c⋅x, m)) = c ⋅ f(vecCons(x, m)).
LaTeX
$$$f(\\mathrm{Matrix}.vecCons(c \\cdot x, m)) = c \\cdot f(\\mathrm{Matrix}.vecCons(x, m))$$$
Lean4
/-- A version of `MultilinearMap.cons_smul` for `AlternatingMap`. -/
theorem map_vecCons_smul {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (c : R) (x : M) :
f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m) :=
f.toMultilinearMap.cons_smul _ _ _