rTensor_tensor — Mathlib

English

The inverse associator for the higher associator in the tensor product setting is given by swapping the groupings and applying the inverse associator.

Русский

Обратный ассоциатор для более высокого уровня ассоциатора в тензорном произведении задаётся перестановкой скобок и применением обратного ассоциатора.

LaTeX

$$$(\\text{tensorTensorTensorAssoc } R M N P Q)^{-1} = \\text{tensorTensorTensorAssoc } R M P N Q$$$

Lean4

theorem rTensor_tensor : rTensor (M ⊗[R] N) g = assoc R Q M N ∘ₗ rTensor N (rTensor M g) ∘ₗ (assoc R P M N).symm :=
  TensorProduct.ext <| LinearMap.ext fun _ ↦ TensorProduct.ext rfl

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