English
Let g be a multilinear map and for every index i let f_i be a linear map from M_i to M_i'. Then the multilinear map obtained by composing g with each f_i in the corresponding argument evaluates at m = (m_i) as g(i ↦ f_i(m_i)). In other words, applying the composed map to m yields the same as applying g to the vector of images f_i(m_i).
Русский
Пусть g — мультилинейная карта, и для каждого индекса i задан линейный переход f_i: M_i → M_i'. Тогда параллельно с каждым аргументом выполняется композиция: отображение g_compLinearMap_f применяется к m = (m_i) так же, как и g, но с аргументами f_i(m_i). Другими словами, значение (g ∘ f)(m) равно g( i ↦ f_i(m_i) ).
LaTeX
$$$ (g.compLinearMap f)\\; m \\\\stackrel{?}{=} g \\bigl( i \\mapsto f i (m i) \\bigr) $$$
Lean4
@[simp]
theorem compLinearMap_apply (g : MultilinearMap R M₁' M₂) (f : ∀ i, M₁ i →ₗ[R] M₁' i) (m : ∀ i, M₁ i) :
g.compLinearMap f m = g fun i => f i (m i) :=
rfl
