English
For a multilinear map f over a family of modules, applying scalar multipliers c_i to each coordinate yields the same as multiplying the overall result by the product of c_i.
Русский
Для мультилинейного отображения сумма координат умножений даёт тот же результат, что и произведение скаляров.
LaTeX
$$$f(\\lambda i. c_i \\cdot m_i) = (\\prod_i c_i) \\cdot f(m).$$$
Lean4
/-- A bilinear map into `Fin n.succ → M₃` can be built out of a map into `M₃` and a map into
`Fin n → M₃` -/
@[simps]
def vecCons₂ {n} (f : M →ₗ[R] M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃) : M →ₗ[R] M₂ →ₗ[R] Fin n.succ → M₃
where
toFun m := LinearMap.vecCons (f m) (g m)
map_add' x
y :=
LinearMap.ext fun z => by
simp only [f.map_add, g.map_add, LinearMap.add_apply, LinearMap.vecCons_apply, Matrix.cons_add_cons (f x z)]
map_smul' r x := LinearMap.ext fun z => by simp [Matrix.smul_cons r (f x z)]
