Mathlib v3 is deprecated. Go to Mathlib v4

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
added theorem linear_map.coe_fn_sum
added theorem bilin_form.add_apply
added theorem bilin_form.coe_fn_mk
added def bilin_form.comp
added theorem bilin_form.comp_apply
added theorem bilin_form.smul_apply
added theorem quadratic_form.ext
added theorem quadratic_form.map_neg
added theorem quadratic_form.map_sub
added structure quadratic_form