Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quadratic_form.pos_def_of_nonneg

Modification history

2021-12-22 23:07
src/linear_algebra/quadratic_form/basic.lean
feat(quadratic_form/prod): quadratic forms on product and pi types (#10939) …
Added quadratic_form.pos_def_of_nonnegView on Github →