lTensorOne_one_tmul — Mathlib

English

For y ∈ R and m ∈ M, the map M.lTensorOne' sends m ⊗ (algebraMap y) to y m, i.e., scalar multiplication via the left action.

Русский

Для y ∈ R и m ∈ M отображение M.lTensorOne' отправляет m ⊗ (algebraMap y) в y m, то есть лево-скалярное умножение.

LaTeX

$$$M.lTensorOne'(m \\otimes_R \\text{algebraMap}_R^S(y)) = y \\cdot m$$$

Lean4

@[simp]
theorem lTensorOne_one_tmul (n : N) : N.lTensorOne (1 ⊗ₜ[R] n) = n :=
  N.lTensorOne'_one_tmul n

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