Def PerfectPairing.mkOfInjective

Modification history

2025-01-15 22:33
Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
chore: split file `LinearAlgebra.PerfectPairing` (#20780) …
Modified PerfectPairing.mkOfInjectiveView on Github →
2024-11-07 11:59
Mathlib/LinearAlgebra/PerfectPairing.lean
feat: define restrictions of perfect pairings (#18559) …
Added PerfectPairing.mkOfInjectiveView on Github →