Def Matrix.toPerfectPairing

Modification history

2025-12-29 03:44

Mathlib/LinearAlgebra/PerfectPairing/Matrix.lean

chore: remove May 2025 deprecated declarations (#33014) …

Deleted Matrix.toPerfectPairing View on Github →

2025-06-07 19:11

Mathlib/LinearAlgebra/PerfectPairing/Matrix.lean

feat: an invertible matrix as a perfect pairing (#25477) …

Added Matrix.toPerfectPairing View on Github →