mathlib3

fa7b5f20 - feat(linear_algebra/quadratic_form): Complex version of Sylvester's law of inertia (#7416)

feat(linear_algebra/quadratic_form): Complex version of Sylvester's law of inertia (#7416) Every nondegenerate complex quadratic form is equivalent to a quadratic form corresponding to the sum of squares.