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