map_vecCons_smul — Mathlib

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 _ _ _

Похожие утверждения