Commit 2021-09-30 08:02 f31758a8

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_forms to quadratic_forms. 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.