coe_rTensorHom — Mathlib

English

The right-tensoring by M on maps coincides with the canonical right-tensor operation: applying rTensor M to f is the same as the canonical rTensor map.

Русский

Правое тензорное отображение по M на отображения совпадает с каноническим правым тензорным отображением: применение rTensor M к f равно каноническому отображению rTensor.

LaTeX

$$$(rTensorHom\,M) = rTensor\,M$$$

Lean4

@[simp]
theorem coe_rTensorHom : (rTensorHom M : (N →ₗ[R] P) → N ⊗[R] M →ₗ[R] P ⊗[R] M) = rTensor M :=
  rfl

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