Commit 2021-06-07 15:40 fa7b5f20View on Github →
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.
added theorem quadratic_form.basis_repr_apply
added theorem quadratic_form.equivalent_sum_squares
added theorem quadratic_form.isometry_of_is_Ortho_apply
added def quadratic_form.weighted_sum_squares
added theorem quadratic_form.weighted_sum_squares_apply