English
The coercion with scalar multiplication distributes over product of multilinear maps; the equality aligns the scalar action with evaluation.
Русский
Коэрсионная связь со скаляром распространяется на произведение мультилейных отображений; равенство согласует скалярное действие с оценкой.
LaTeX
$$$ f( c • m ) = c • f(m) $ как формальная запись$$
Lean4
/-- If `g` is a multilinear map and `f` is a collection of linear maps,
then `g (f₁ m₁, ..., fₙ mₙ)` is again a multilinear map, that we call
`g.compLinearMap f`. -/
def compLinearMap (g : MultilinearMap R M₁' M₂) (f : ∀ i, M₁ i →ₗ[R] M₁' i) : MultilinearMap R M₁ M₂
where
toFun m := g fun i => f i (m i)
map_update_add' m i x
y :=
by
have : ∀ j z, f j (update m i z j) = update (fun k => f k (m k)) i (f i z) j := fun j z =>
Function.apply_update (fun k => f k) _ _ _ _
simp [this]
map_update_smul' m i c
x :=
by
have : ∀ j z, f j (update m i z j) = update (fun k => f k (m k)) i (f i z) j := fun j z =>
Function.apply_update (fun k => f k) _ _ _ _
simp [this]
