dualTensorHom_apply — Mathlib

English

On a simple tensor f ⊗ m, the map dualTensorHom sends to the linear map m' ↦ f(m')·m.

Русский

На простом тензоре f ⊗ m отображение dualTensorHom отправляет в линейное отображение m' ↦ f(m')·m.

LaTeX

$$$\big(\mathrm{dualTensorHom}(R,M,N)(f \otimes m)\big)(m') = f(m')\,m$$$

Lean4

@[simp]
theorem dualTensorHom_apply (f : Module.Dual R M) (m : M) (n : N) : dualTensorHom R M N (f ⊗ₜ n) m = f m • n :=
  rfl

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