rTensor_lTensor_comp_assoc_symm — Mathlib

English

A symmetric companion of the previous associativity identity holds with the inverse of the associator: rTensor Q (lTensor P x) ∘ₗ (TensorProduct.assoc R P M Q).symm = (TensorProduct.assoc R P N Q).symm ∘ₗ lTensor P (rTensor Q x).

Русский

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

LaTeX

$$$ rTensor Q (lTensor P x) \\circ \\big( TensorProduct.assoc R P M Q \\big).symm = \\big( TensorProduct.assoc R P N Q \\big).symm \\circ lTensor P (rTensor Q x). $$$

Lean4

theorem rTensor_lTensor_comp_assoc_symm (x : M →ₗ[R] N) :
    rTensor Q (lTensor P x) ∘ₗ (TensorProduct.assoc R P M Q).symm =
      (TensorProduct.assoc R P N Q).symm ∘ₗ lTensor P (rTensor Q x) :=
  by simp_rw [rTensor, lTensor, map_map_comp_assoc_symm_eq]

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