Commit 2025-06-07 19:11 6f872f1d

feat: an invertible matrix as a perfect pairing (#25477) Using this we can do things like:

attribute [simp] Matrix.one_fin_two
#check !![2, -3; -1, 2].toPerfectPairing ⟨!![2, 3; 1, 2], by simp, by simp⟩ -- Works