dual — Mathlib

English

A perfect pairing p on M,N induces a perfect pairing on their duals, giving a canonically defined PerfectPairing R (Dual M) (Dual N).

Русский

Идеальная пара между M и N индуцирует идеальную пару на их двойственных пространствах.

LaTeX

$$$\text{PerfectPairing}(R, \\mathrm{Dual}(R,M), \\mathrm{Dual}(R,N))$ via p.$$

Lean4

/-- A perfect pairing induces a perfect pairing between dual spaces. -/
@[deprecated "No replacement" (since := "2025-05-27")]
def dual (p : PerfectPairing R M N) : PerfectPairing R (Dual R M) (Dual R N) :=
  let _i := p.reflexive_right
  (p.toDualRight.symm.trans (evalEquiv R N)).toPerfectPairing

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