contractRight — Mathlib

English

There is a natural bilinear pairing between a module and its dual, sending m ⊗ g to g(m).

Русский

Существует естественное билинейное сопоставление между модулем и его двойственным, отправляющее m ⊗ g в g(m).

LaTeX

$$$\langle m, g\rangle = g(m)$ for $g ∈ M^*$ and $m ∈ M$.$$

Lean4

/-- The natural right-handed pairing between a module and its dual. -/
def contractRight : M ⊗[R] Module.Dual R M →ₗ[R] R :=
  (uncurry _ _ _ _).toFun (LinearMap.flip LinearMap.id)

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