mathlib3
6e0e270d - feat(linear_algebra/matrix): positive definite (#14531)

Commit

3 years ago

feat(linear_algebra/matrix): positive definite (#14531) Define positive definite matrices and connect them to positive definiteness of quadratic forms.

Author

abentkamp

Parents

784c7034

mathlib3 6e0e270d - feat(linear_algebra/matrix): positive definite (#14531)

mathlib3
6e0e270d - feat(linear_algebra/matrix): positive definite (#14531)