assoc_symm_tmul — Mathlib

English

The inverse associator satisfies the inverse relation on simple tensors: (assoc R S A C D)^{-1} (x ⊗_S (y ⊗_R z)) = (x ⊗_S y) ⊗_R z.

Русский

Обратный ассоциатор удовлетворяет обратному равенству на простых тензорах: (assoc)^{-1}(x ⊗_S (y ⊗_R z)) = (x ⊗_S y) ⊗_R z.

LaTeX

$$$\big(\text{assoc}_{R,S,A,C,D}\big)^{-1} (x \otimes_S (y \otimes_R z)) = (x \otimes_S y) \otimes_R z$$$

Lean4

@[simp]
theorem assoc_symm_tmul (x : A) (y : C) (z : D) :
    (Bialgebra.TensorProduct.assoc R S A C D).symm (x ⊗ₜ (y ⊗ₜ z)) = (x ⊗ₜ y) ⊗ₜ z :=
  rfl

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