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 _ _ _