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.





leanprover-community/mathlib,leanprover-community/mathlib