dualEval

Mathlib.LinearAlgebra.PerfectPairing.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.IsPerfPair.dualEval

English

If M is reflexive, then the evaluation pairing on Dual_R M is a perfect pairing.

Русский

Если M является рефлексивным, то оценочная пара между Dual_R M и M является совершенной парой.

LaTeX

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

Lean4

/-- A reflexive module has a perfect pairing with its dual. -/
instance dualEval [IsReflexive R M] : IsPerfPair (Dual.eval R M) :=
  .flip .id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru