English
The construction mapLMultilinear provides a continuous multilinear map that sends a family of linear maps to a multilinear map on the tensor product; its toFun encodes the expected tensor product action.
Русский
Конструкция mapLMultilinear задаёт непрерывную мультилейную карту, которая отправляет семейство линейных отображений в мультилейную карту на тензорное произведение; её функция toFun кодирует ожидаемое действие на тензоре.
LaTeX
$$$ \\mathrm{mapLMultilinear} : \\big(\\lambda i, E_i \\toL[𝕜] E'_i\\big) \\to \\big( (⨂[𝕜] i, E_i) \\toL[𝕜] (⨂[𝕜] i, E'_i) \\big) $$$
Lean4
protected theorem mapL_smul [DecidableEq ι] (i : ι) (c : 𝕜) (u : E i →L[𝕜] E' i) :
mapL (update f i (c • u)) = c • mapL (update f i u) :=
by
ext x
simp only [mapL_apply, mapL_add_smul_aux, ContinuousLinearMap.coe_smul, PiTensorProduct.map_update_smul,
LinearMap.smul_apply, ContinuousLinearMap.coe_smul', Pi.smul_apply]
