tmul — Mathlib

English

If R,A are rings with appropriate structure, the action of tensorDistrib on tmul reduces to bilinear action on components.

Русский

Действие tensorDistrib на tmul сводится к билинейному действию на компонентах.

LaTeX

$$$\\text{tensorDistrib}\\ R\\ A (Q_1 \\otimes_\\text{tmul} Q_2)\\ (m_1 \\otimes_\\! m_2) = Q_1(m_1) \\otimes_\\! Q_2(m_2)$$$

Lean4

/-- The tensor product of two quadratic maps, a shorthand for dot notation. -/
protected abbrev tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) :
    QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
  tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂)

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