Commit 2020-06-05 10:10 1ef65c99View 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
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.