# Commit 2020-06-05 10:10 1ef65c99

View on Github →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.