mathlib

eb9bd55f - feat(linear_algebra/quadratic_form): Real version of Sylvester's law of inertia (#7427)

feat(linear_algebra/quadratic_form): Real version of Sylvester's law of inertia (#7427) We prove that every nondegenerate real quadratic form is equivalent to a weighted sum of squares with the weights being ±1.