Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quadratic_form.nonneg_pi_iff

Modification history

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