English
Let (s_i) be a family of R-modules. There exists a canonical multilinear map tprod from the family to the tensor product ⨂[R] i, s_i, defined by tprod(f) = tprodCoeff R 1 f.
Русский
Пусть (s_i) есть семейство модулей над R. Существование канонического многолинейного отображения tprod от этой семьи в тензорное произведение ⨂[R] i, s_i, задаётся как tprod(f) = tprodCoeff R 1 f.
LaTeX
$$$$ tprod = tprodCoeff(R,\,1) $$$$
Lean4
/-- The canonical `MultilinearMap R s (⨂[R] i, s i)`.
`tprod R fun i => f i` has notation `⨂ₜ[R] i, f i`. -/
def tprod : MultilinearMap R s (⨂[R] i, s i) where
toFun := tprodCoeff R 1
map_update_add' {_ f} i x y := (add_tprodCoeff (1 : R) f i x y).symm
map_update_smul' {_ f} i r x := by rw [smul_tprodCoeff', ← smul_tprodCoeff (1 : R) _ i, update_idem, update_self]
