tensorAssoc_apply — Mathlib

English

The underlying linear map of the associativity isometry is exactly the canonical associativity map on the triple tensor product.

Русский

Базовая линейная карта изометрии ассоциации совпадает с канонической картой ассоциативности на тройном тензорном произведении.

LaTeX

$$$\text{toLinearEquiv}(\text{tensorAssoc}(Q_1,Q_2,Q_3)) = \text{TensorProduct}.assoc(R,M_1,M_2,M_3).$$$

Lean4

@[simp]
theorem tensorAssoc_apply (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃)
    (x : (M₁ ⊗[R] M₂) ⊗[R] M₃) : tensorAssoc Q₁ Q₂ Q₃ x = TensorProduct.assoc R M₁ M₂ M₃ x :=
  rfl

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