zero — Mathlib

English

The tensor product M ⊗_R N carries a canonical zero element, making it an additive object; a pure tensor with a zero component is zero: 0 ⊗ n = 0 for all n ∈ N and m ⊗ 0 = 0 for all m ∈ M.

Русский

У тензорного произведения есть канонический нулевой элемент; чистый тензор с нулевым компонентом равен нулю: 0 ⊗ n = 0 и m ⊗ 0 = 0.

LaTeX

$$$ (0) = 0 \\;\\in\\; M \\otimes_R N, \\quad 0 ⊗ n = 0, \\quad m ⊗ 0 = 0. $$$

Lean4

protected instance zero : Zero (M ⊗[R] N) :=
  (addConGen (TensorProduct.Eqv R M N)).zero

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