tensorAssoc_symm_apply — Mathlib

English

The inverse associativity map coincides with the standard inverse associativity on the triple tensor product.

Русский

Обратная карта ассоциативности совпадает с обычной обратной картой ассоциативности на тройном тензорном произведении.

LaTeX

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

Lean4

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

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