tmul — Mathlib

English

The tensor product of two bilinear forms is a bilinear form on the tensor product of the underlying modules, written as B1.tm ul B2.

Русский

Тензорное произведение двух билинейных форм является билинейной формой на тензорном произведении соответствующих модулей.

LaTeX

$$$$\text{tmul}(B_1,B_2) : BilinForm \; A\; (M_1 \otimes_R M_2) \to A,$$$$

Lean4

/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/
protected abbrev tmul (B₁ : BilinForm A M₁) (B₂ : BilinMap R M₂ R) : BilinMap A (M₁ ⊗[R] M₂) A :=
  tensorDistrib R A (B₁ ⊗ₜ[R] B₂)

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