dualPairing — Mathlib

English

There is a canonical pairing between a vector space and its dual, given by evaluation.

Русский

Существует каноническое парирование между пространством и его двойственным, задаваемое оценкой.

LaTeX

$$$ \\mathrm{dualPairing} (R,M) : \\mathrm{Dual}R M \\to M \\to R $$$

Lean4

/-- The canonical pairing of a vector space and its algebraic dual. -/
def dualPairing (R M) [CommSemiring R] [AddCommMonoid M] [Module R M] : Module.Dual R M →ₗ[R] M →ₗ[R] R :=
  LinearMap.id

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