leftComm_symm_tmul — Mathlib

English

A symmetric version of the associator compatibility: the two ways of regrouping maps coincide after applying the symmetry of the associator.

Русский

Симметричная версия совместимости: два способа перестройки группировок отображений совпадают после применения симметрии ассоциатора.

LaTeX

$$$(f\\otimes g) h \\circ\\alpha_{M,N,P}^{-1} = \\alpha_{Q,S,T}^{-1} \\circ (f\\otimes (g\\otimes h))$$$

Lean4

@[simp]
theorem leftComm_symm_tmul (m : M) (n : N) (p : P) : (leftComm R M N P).symm (n ⊗ₜ (m ⊗ₜ p)) = m ⊗ₜ (n ⊗ₜ p) :=
  rfl

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