tmul_add — Mathlib

English

The tmul function is the canonical bilinear map sending a pair to the tensor product, i.e., m ⊗ n.

Русский

Функция tmul — каноническое билинейное отображение, отправляющее пару в тензорное произведение, то есть m ⊗ n.

LaTeX

$$$ \\mathrm{tmul}(m,n) = m \\otimes_R n. $$$

Lean4

theorem tmul_add (m : M) (n₁ n₂ : N) : m ⊗ₜ (n₁ + n₂) = m ⊗ₜ n₁ + m ⊗ₜ[R] n₂ :=
  Eq.symm <| Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_add_right _ _ _

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