tmul — Mathlib

English

There is a canonical bilinear map tmul: M × N → M ⊗_R N given by tmul(m,n) = m ⊗ n, which identifies the tensor product with the formal symbol m ⊗ n.

Русский

Существует каноническое билинеарное отображение tmul: M × N → M ⊗_R N, определяемое как tmul(m,n) = m ⊗ n, задающее тензорное произведение.

LaTeX

$$$\\mathrm{tmul}: M \\times N \\to M \\otimes_R N, \\quad \\mathrm{tmul}(m,n)=m\\otimes n$$$

Lean4

/-- The canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`. -/
def tmul (m : M) (n : N) : M ⊗[R] N :=
  AddCon.mk' _ <| FreeAddMonoid.of (m, n)

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