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

Estimated changes