Commit 2021-11-17 09:02 c7441af1
View on Github →feat(linear_algebra/bilinear_form): add lemmas about congr (#10362)
With these some of the nondegenerate proofs can be golfed to oblivion, rather than reproving variants of the same statement over and over again.