assoc_symm_tmul — Mathlib

English

The underlying linear map of the associator coincides with the standard linear associator on tensor products.

Русский

Покрывающая линейная карта ассоциатора совпадает с стандартной линейной ассоциаторной картой на тензорном произведении.

LaTeX

$$$ (\\operatorname{assoc}_{R,S,A,C,D})^{\\mathrm{toLinearEquiv}} = \\operatorname{AlgebraTensorModule.assoc}_{R,S,S,A,C,D} $$$

Lean4

@[simp]
theorem assoc_symm_tmul (a : A) (b : C) (c : D) :
    (TensorProduct.assoc R S A C D).symm (a ⊗ₜ (b ⊗ₜ c)) = (a ⊗ₜ b) ⊗ₜ c :=
  rfl

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