English
If f is a family of linear maps, then sending a multilinear map g to g(f1 ⬝, ..., fn ⬝) is linear in g.
Русский
Если f — семейство линейных отображений, то отображение g ↦ g(f1 ⬝, …, fn ⬝) линейно по g.
LaTeX
$$$$\text{compLinearMap}_{f}(g) = g \circ f, \quad \text{so } \text{compLinearMap}_{f}(\alpha g_1 + \beta g_2) = \alpha \text{compLinearMap}_{f}(g_1) + \beta \text{compLinearMap}_{f}(g_2).$$$$
Lean4
/-- If `f` is a collection of linear maps, then the construction `MultilinearMap.compLinearMap`
sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g`. -/
@[simps]
def compLinearMapₗ (f : Π (i : ι), M₁ i →ₗ[R] M₁' i) : (MultilinearMap R M₁' M₂) →ₗ[R] MultilinearMap R M₁ M₂
where
toFun := fun g ↦ g.compLinearMap f
map_add' := fun _ _ ↦ rfl
map_smul' := fun _ _ ↦ rfl
