English
Let g be a linear map from M2 to M3 and f be a multilinear map from {M1 i} to M2. Then the composition g ∘ f defines a multilinear map from {M1 i} to M3; i.e., the composition of a multilinear map with a linear map is multilinear.
Русский
Пусть g — линейное отображение от M2 в M3, а f — мультилнейное отображение из семейства {M1 i} в M2. Тогда композиция g ∘ f задаёт мультилнейшее отображение от {M1 i} в M3; то есть композиция мультиленейного отображения с линейным отображением сохраняет мультиленейность.
LaTeX
$$$\text{compMultilinearMap}(g,f) \in \operatorname{MultilinearMap} \; R \; M_1 \; M_3$, where toFun($\text{compMultilinearMap}(g,f)$) = $g \circ f$; hence the map $m \mapsto g(f(m))$ is multilinear in each argument.$$
Lean4
/-- Composing a multilinear map with a linear map gives again a multilinear map. -/
def compMultilinearMap (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) : MultilinearMap R M₁ M₃
where
toFun := g ∘ f
map_update_add' m i x y := by simp
map_update_smul' m i c x := by simp
