mathlib3

1ef65c99 - feat(linear_algebra/quadratic_form): more constructions for quadratic forms (#2949)

feat(linear_algebra/quadratic_form): more constructions for quadratic forms (#2949) Define multiplication of two linear forms to give a quadratic form and addition of quadratic forms. With these definitions, we can write a generic binary quadratic form as `a • proj R₁ 0 0 + b • proj R₁ 0 1 + c • proj R₁ 1 1 : quadratic_form R₁ (fin 2 → R₁)`. In order to prove the linearity conditions on the constructions, there are new `simp` lemmas `polar_add_left`, `polar_smul_left`, `polar_add_right` and `polar_smul_right` copying from the corresponding fields of the `quadratic_form` structure, that use `⇑ Q` instead of `Q.to_fun`. The original field names have a `'` appended to avoid name clashes.