English
If g is multilinear and f1, f2 are linear maps applied coordinatewise, then composing g with f1 and then with f2 is the same as composing g directly with the per-coordinate composition f1 i ∘ f2 i.
Русский
Если g — мультилитейная карта, а f1 и f2 — линейные отображения, применяемые по каждой координате, то (g ∘ f1) ∘ f2 = g ∘ (i ↦ f1 i ∘ f2 i).
LaTeX
$$$(g.compLinearMap f_1).compLinearMap f_2 = g.compLinearMap (\\λ i, f_1 i ∘_l f_2 i) $$$
Lean4
/-- Composing a multilinear map twice with a linear map in each argument is
the same as composing with their composition. -/
theorem compLinearMap_assoc (g : MultilinearMap R M₁'' M₂) (f₁ : ∀ i, M₁' i →ₗ[R] M₁'' i) (f₂ : ∀ i, M₁ i →ₗ[R] M₁' i) :
(g.compLinearMap f₁).compLinearMap f₂ = g.compLinearMap fun i => f₁ i ∘ₗ f₂ i :=
rfl
