coe_lTensorHom — Mathlib

English

Let M be a module and f a linear map N → P. The left-tensoring by M on maps coincides with the canonical left-tensor operation: applying lTensorHom M to f gives the same map as lTensor M applied to f.

Русский

Пусть M — модуль и f — линейное отображение N → P. Левое тензорирование по M на отображения совпадает с каноническим левосторонним тензорным отображением: применение lTensorHom M к f дает то же отображение, что и lTensor M к f.

LaTeX

$$$(lTensorHom\,M) = lTensor\,M$$$

Lean4

@[simp]
theorem coe_lTensorHom : (lTensorHom M : (N →ₗ[R] P) → M ⊗[R] N →ₗ[R] M ⊗[R] P) = lTensor M :=
  rfl

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