id — Mathlib · SciLib

English

If M is reflexive, then the pairing between Dual_R M and M given by evaluation is a perfect pairing.

Русский

Пусть M — рефлексивный модуль над R. Тогда пара между Dual_R M и M, заданная оцениванием, является совершенной парой.

LaTeX

$$$\mathrm{IsPerfPair}(\mathrm{Dual.eval}\ R\ M)$$$

Lean4

/-- A reflexive module has a perfect pairing with its dual. -/
protected instance id [IsReflexive R M] : IsPerfPair (.id (R := R) (M := Dual R M))
    where
  bijective_left := bijective_id
  bijective_right := bijective_dual_eval R M

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