Commit 2020-04-24 11:13 3ae22de4
View 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 data/matrix/basic.lean
and linear_algebra/bilinear_form.lean
and did some cleaning up.