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.

Estimated changes

added theorem matrix.col_add
added theorem matrix.col_mul_vec
added theorem matrix.col_smul
added theorem matrix.col_val
added theorem matrix.col_vec_mul
added theorem matrix.mul_vec_mul_vec
added theorem matrix.mul_vec_zero
added theorem matrix.row_add
added theorem matrix.row_mul_vec
added theorem matrix.row_smul
added theorem matrix.row_val
added theorem matrix.row_vec_mul
added theorem matrix.transpose_col
added theorem matrix.transpose_row
added theorem matrix.vec_mul_one
added theorem matrix.vec_mul_vec_mul
added theorem matrix.vec_mul_zero