rTensorOne'_tmul_one — Mathlib

English

The map rTensorOne' sends m ⊗ 1 to m; in particular, applying it to a pure tensor with 1 yields the original module element.

Русский

Отображение rTensorOne' отправляет m ⊗ 1 в m; применение к простому тензору с единицей возвращает исходный элемент модуля.

LaTeX

$$$M.rTensorOne'(m \\otimes_R 1) = m$$$

Lean4

@[simp]
theorem rTensorOne'_tmul_one (m : M) : M.rTensorOne' (m ⊗ₜ[R] 1) = m := by simpa using rTensorOne'_tmul 1 m

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