lTensor_def — Mathlib

English

For a linear map f: N → P, the map lTensor M f is the natural map M ⊗ N → M ⊗ P given by TensorProduct.map id f.

Русский

Для линейного отображения f: N → P отображение lTensor M f — естественное отображение M ⊗ N → M ⊗ P, заданное TensorProduct.map id f.

LaTeX

$$$ lTensor\\ M\\ f = TensorProduct.map\\ id\\ f $$$

Lean4

theorem lTensor_def : f.lTensor M = TensorProduct.map LinearMap.id f :=
  rfl

Похожие утверждения