English
Associativity holds for the PiTensorProduct multiplication: mul (mul x y) z = mul x (mul y z).
Русский
Сопряженное умножение по PiTensorProduct ассоциативно: mul (mul x y) z = mul x (mul y z).
LaTeX
$$$mul\\ (mul\\ x\\ y)\\ z = mul\\ x\\ (mul\\ y\\ z)$$$
Lean4
protected theorem mul_assoc (x y z : ⨂[R] i, A i) : mul (mul x y) z = mul x (mul y z) := by
-- restate as an equality of morphisms so that we can use `ext`
suffices
LinearMap.llcomp R _ _ _ mul ∘ₗ mul =
(LinearMap.llcomp R _ _ _ LinearMap.lflip.toLinearMap <| LinearMap.llcomp R _ _ _ mul.flip ∘ₗ mul).flip
by exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z
ext x y z
dsimp [← mul_def]
simpa only [tprod_mul_tprod] using congr_arg (tprod R) (mul_assoc x y z)
