Documentation

Mathlib.LinearAlgebra.QuadraticForm.Real

Real quadratic forms #

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 nondegenerate we can take the weights to be ±1, as in equivalent_one_zero_neg_one_weighted_sum_squared.

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
  • One or more equations did not get rendered due to their size.
Instances For

    Sylvester's law of inertia: A nondegenerate real quadratic form is equivalent to a weighted sum of squares with the weights being ±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.