mathlib

c7441af1 - feat(linear_algebra/bilinear_form): add lemmas about congr (#10362)

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.