toPerfectPairing — Mathlib

English

A short identity expressing that the transitive composition of a dual map with the flip yields the evaluation map on N.

Русский

Краткое тождество: композиция двойственной карты и flip дает оценку на N.

LaTeX

$$$e\\,\\text{trans}\\, e.flip.symm.dualMap = \\mathrm{Dual.eval}(R,N)$$$

Lean4

/-- If `M` is reflexive then a linear equivalence `N ≃ Dual R M` is a perfect pairing. -/
@[deprecated "No replacement" (since := "2025-05-27")]
def toPerfectPairing : PerfectPairing R N M where
  toLinearMap := e
  bijective_left := e.bijective
  bijective_right := e.flip.bijective

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