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.
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
