assoc_symm_tmul — Mathlib

English

For a ∈ P, the inverse of the lid map sends a to 1 ⊗ a in M ⊗ R P; i.e., (lid_R P)^{-1}(a) = 1 ⊗ a.

Русский

Обратное к lid отображение отправляет a в 1 ⊗ a в M ⊗_R P; то есть (lid_R P)^{-1}(a) = 1 ⊗ a.

LaTeX

$$$ (\mathrm{Coalgebra.TensorProduct.lid}\; R\; P)^{-1}(a) = 1 \otimes a . $$$

Lean4

@[simp]
theorem assoc_symm_tmul (x : M) (y : N) (z : P) :
    (Coalgebra.TensorProduct.assoc R S M N P).symm (x ⊗ₜ (y ⊗ₜ z)) = (x ⊗ₜ y) ⊗ₜ z :=
  rfl

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