toPerfectPairingDual — Mathlib

English

If M is reflexive, then a linear equivalence e: N ≃ Dual M yields a perfect pairing between N and M.

Русский

Если M рефлексивен, то линейное эквивалентное отображение e: N ≃ Dual M задаёт идеальную пару между N и M.

LaTeX

$$$\text{ToPerfectPairing}(e): \text{PerfectPairing } R\,N\,M$.$$

Lean4

/-- A reflexive module has a perfect pairing with its dual. -/
@[deprecated LinearMap.IsPerfPair.id (since := "2025-05-27")]
def toPerfectPairingDual : PerfectPairing R (Dual R M) M
    where
  toLinearMap := .id
  bijective_left := bijective_id
  bijective_right := bijective_dual_eval R M

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