English
The associator map satisfies a multiplicativity-like law on simple tensors: assoc((a1 a2) ⊗ (b1 b2) ⊗ (c1 c2)) equals the product of assoc(a1 ⊗ b1 ⊗ c1) and assoc(a2 ⊗ b2 ⊗ c2).
Русский
Ассоциатор удовлетворяет закону, аналогичному умножению, на простых тензорах: assoc((a1 a2) ⊗ (b1 b2) ⊗ (c1 c2)) = assoc(a1 ⊗ b1 ⊗ c1) · assoc(a2 ⊗ b2 ⊗ c2).
LaTeX
$$$ \\operatorname{assoc}_{R,A,B,C}( (a_1 a_2) \\otimes (b_1 b_2) \\otimes (c_1 c_2) ) = \\operatorname{assoc}_{R,A,B,C}(a_1 \\otimes b_1 \\otimes c_1) \\cdot \\operatorname{assoc}_{R,A,B,C}(a_2 \\otimes b_2 \\otimes c_2) $$$
Lean4
theorem assoc_aux_1 (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C) :
(TensorProduct.assoc R A B C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) =
(TensorProduct.assoc R A B C) (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) * (TensorProduct.assoc R A B C) (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂) :=
rfl
