rightComm_symm — Mathlib

English

The inverse associator acts on a simple tensor by rebracketing in the opposite direction: (m ⊗ (n ⊗ p)) maps to (m ⊗ n) ⊗ p under the inverse associator.

Русский

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

LaTeX

$$$(\\text{assoc}_R(M,N,P)^{-1})(m\\otimes_R (n\\otimes_R p)) = (m\\otimes_R n)\\otimes_R p$$$

Lean4

@[simp]
theorem rightComm_symm : (rightComm R M N P).symm = rightComm R M P N :=
  rfl

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