tmul_comp_tensorAssoc — Mathlib

English

Associativity of tmul on triple tensor products: (Q1.tmul (Q2.tmul Q3)) on TensorProduct.assoc equals (Q1.tmul Q2).tmul Q3.

Русский

Ассоциативность tmul над тройным тензорным произведением: (Q1.tmul (Q2.tmul Q3)) на TensorProduct.assoc равно (Q1.tmul Q2).tmul Q3.

LaTeX

$$$\\big(Q_1 \\tmul (Q_2 \\tmul Q_3)\\big) \\circ \\mathrm{TensorProduct}.assoc = (Q_1 \\tmul Q_2) .tmul Q_3$$$

Lean4

@[simp]
theorem tmul_comp_tensorAssoc (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃) :
    (Q₁.tmul (Q₂.tmul Q₃)).comp (TensorProduct.assoc R M₁ M₂ M₃) = (Q₁.tmul Q₂).tmul Q₃ :=
  by
  refine (QuadraticMap.associated_rightInverse R).injective ?_
  ext m₁ m₂ m₁' m₂' m₁'' m₂''
  dsimp [-associated_apply]
  simp only [associated_tmul, QuadraticMap.associated_comp]
  exact mul_assoc _ _ _

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