Commit 2020-04-24 11:13 3ae22de4View on Github →
feat(linear_algebra): quadratic forms (#2480)
Define quadratic forms over a module, maps from quadratic forms to bilinear forms and matrices, positive definite quadratic forms and the discriminant of quadratic forms.
Along the way, I added some definitions to
linear_algebra/bilinear_form.lean and did some cleaning up.