rid_symm_apply — Mathlib

English

The inverse of the canonical rid isomorphism on M decomposes as m maps to m ⊗ 1, i.e. (rid R A M)^{-1}(m) = m ⊗ 1.

Русский

Обратное к каноническому изоморфизму rid на M разлагается так: для элемента m выполняется (rid R A M)^{-1}(m) = m ⊗ 1.

LaTeX

$$$\bigl(\operatorname{rid} R A M\bigr)^{-1}(m) = m \otimes 1$$$

Lean4

@[simp]
theorem rid_symm_apply (m : M) : (AlgebraTensorModule.rid R A M).symm m = m ⊗ₜ 1 :=
  rfl

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