Def PerfectPairing.toDualLeft

Modification history

2024-11-07 11:59
Mathlib/LinearAlgebra/PerfectPairing.lean
feat: define restrictions of perfect pairings (#18559) …
Added PerfectPairing.toDualLeftView on Github →