rid_symm_apply — Mathlib

English

The inverse of the rid is the map that sends an element a in M to a ⊗ 1 in the tensor product M ⊗ R.

Русский

Обратное отображение rid отправляет элемент a ∈ M в a ⊗ 1 в тензорном произведении M ⊗ R.

LaTeX

$$$ (\mathrm{rid}_{\mathrm{CTP}}(R,S,M))^{-1}(a) = a \otimes_{\mathrm{t}} 1 $$$

Lean4

@[simp]
theorem rid_symm_apply (a : M) : (Coalgebra.TensorProduct.rid R S M).symm a = a ⊗ₜ 1 :=
  rfl

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