Commit 2020-06-05 10:10 1ef65c99

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.