mathlib3
43159737 - feat(quadratic_form/prod): quadratic forms on product and pi types (#10939)

Commit

4 years ago

feat(quadratic_form/prod): quadratic forms on product and pi types (#10939) In order to provide the `pos_def` members, some new API was needed.

Author

eric-wieser

Parents