tmul — Mathlib

English

The base change of a bilinear map B2 along A respects the tmul operation, i.e., B2.baseChange A (a ⊗ m2) (a' ⊗ m2') = (a a') ⊗ (B2 m2 m2').

Русский

Базовое изменение билинейной карты вместе с операцией tmul удовлетворяет тензорному произведению: B2.baseChange A (a ⊗ m2) (a' ⊗ m2') = (a a') ⊗ (B2 m2 m2').

LaTeX

$$$B_2.baseChange\\ A\\ (a\\otimes m_2)\ (a'\\otimes m_2') = (a\\cdot a')\\otimes\\ (B_2\\,m_2\\,m_2').$$$

Lean4

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

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