Def PerfectPairing.restrictScalars

Modification history

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