lTensorOne'_one_tmul — Mathlib

English

There is an R-linear equivalence lTensorOne' between (⊥) ⊗_R N and N, induced by multiplication in S; its inverse sends n to 1 ⊗ n.

Русский

Существуют взаимно однозначные R-линейные отображения между (⊥) ⊗_R N и N, индуцированные умножением в S; обратное отображение отправляет n в 1 ⊗ n.

LaTeX

$$$lTensorOne' : (\bot \otimes_R N) \cong_R N, \quad lTensorOne'^{-1}(n) = 1 \otimes n.$$$

Lean4

@[simp]
theorem lTensorOne'_one_tmul (n : N) : N.lTensorOne' (1 ⊗ₜ[R] n) = n := by simpa using lTensorOne'_tmul 1 n

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