Commit 2025-08-19 11:01 1c5296a7
View on Github →refactor: redefine perfect pairings as a Prop-valued typeclass (#25239)
Redefine perfect pairings using a Prop-valued typeclass IsPerfPair on a bilinear pairing p : M →ₗ[R] N →ₗ[R] R, and a function to turn p : M →ₗ[R] N →ₗ[R] R + p.IsPerfPair into M ≃ₗ[R] Dual R N.
The name IsPerfPair is kept short because it shows up in lemma and definition names.
From Toric