mathlib3documentation

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Sylvester's law of inertia equivalent_one_neg_one_weighted_sum_squared: A real quadratic form is equivalent to a weighted sum of squares with the weights being ±1 or 0.

When the real quadratic form is nondegerate we can take the weights to be ±1, as in equivalent_one_zero_neg_one_weighted_sum_squared.

noncomputable def quadratic_form.isometry_sign_weighted_sum_squares {ι : Type u_1} [fintype ι] [decidable_eq ι] (w : ι ) :

The isometry between a weighted sum of squares with weights u on the (non-zero) real numbers and the weighted sum of squares with weights sign ∘ u.

Equations
theorem quadratic_form.equivalent_one_neg_one_weighted_sum_squared {M : Type u_1} [ M] (Q : M) (hQ : .nondegenerate) :
(w : fin (fdim M) ), ( (i : fin (fdim M)), w i = -1 w i = 1)

Sylvester's law of inertia: A nondegenerate real quadratic form is equivalent to a weighted sum of squares with the weights being ±1.

theorem quadratic_form.equivalent_one_zero_neg_one_weighted_sum_squared {M : Type u_1} [ M] (Q : M) :
(w : fin (fdim M) ), ( (i : fin (fdim M)), w i = -1 w i = 0 w i = 1)

Sylvester's law of inertia: A real quadratic form is equivalent to a weighted sum of squares with the weights being ±1 or 0.