Def Matrix.toPerfectPairing

Modification history

2025-06-07 19:11
Mathlib/LinearAlgebra/PerfectPairing/Matrix.lean
feat: an invertible matrix as a perfect pairing (#25477) …
Added Matrix.toPerfectPairingView on Github →