English
There is a canonical multiplicative structure on A ⊗_R B defined by mul, turning it into a multiplicative object.
Русский
Существует каноническая структура умножения на A ⊗_R B, задаваемая mul.
LaTeX
$$$ \text{Mul} (A \otimes_R B) \text{ defined by } \text{mul}$$$
Lean4
protected theorem mul_assoc (x y z : A ⊗[R] B) : 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 xa xb ya yb za zb
exact congr_arg₂ (· ⊗ₜ ·) (mul_assoc xa ya za) (mul_assoc xb yb zb)
