English
If s_i ≃ₗ t_i for all i, then the tensor products ⨂ s_i and ⨂ t_i are canonically linearly equivalent via the coordinatewise linear equivalences.
Русский
Если для каждого i имеется линейное эквивалентное преобразование s_i ≃ₗ t_i, то тензорные произведения равны по линейной эквивалентности через координатные преобразования.
LaTeX
$$$\exists f : \Pi i, s_i \cong_ℓ t_i,\; (\⨂ i, s_i) \cong_ℂ (\⨂ i, t_i)$$$
Lean4
/-- The tensor of a family of linear maps from `sᵢ` to `tᵢ`, as a multilinear map of
the family.
-/
@[simps]
noncomputable def mapMultilinear : MultilinearMap R (fun (i : ι) ↦ s i →ₗ[R] t i) ((⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i)
where
toFun := map
map_update_smul' _ _ _ _ := PiTensorProduct.map_update_smul _ _ _ _
map_update_add' _ _ _ _ := PiTensorProduct.map_update_add _ _ _ _
