mathlib

f31758a8 - chore(linear_algebra/quadratic_form): add missing lemmas, lift instance, and tweak argument implicitness (#9458)

chore(linear_algebra/quadratic_form): add missing lemmas, lift instance, and tweak argument implicitness (#9458) This adds `{quadratic,bilin}_form.{ext_iff,congr_fun}`, and a `can_lift` instance to promote `bilin_form`s to `quadratic_form`s. The `associated_*` lemmas should have `Q` and `S` explicit as they are not inferable from the arguments. In particular, with `S` implicit, rewriting any of them backwards introduces a lot of noisy subgoals.