rTensorOne_symm_apply — Mathlib

English

Let M be a submodule of S over R. The canonical isomorphism M ≅ M ⊗_R S has inverse given by M.rTensorOne.symm, and on elements m ∈ M this inverse sends m to m ⊗_R 1.

Русский

Пусть M — подмодуль S над R. Канонический изоморфизм M ≅ M ⊗_R S имеет обратное отображение, заданное через M.rTensorOne.symm: для элемента m ∈ M оно отправляет m на m ⊗_R 1.

LaTeX

$$$M.rTensorOne.symm(m) = m \\otimes_R 1 \\quad (m \\in M).$$$

Lean4

@[simp]
theorem rTensorOne_symm_apply (m : M) : M.rTensorOne.symm m = m ⊗ₜ[R] 1 :=
  rfl

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