Commit 2021-06-11 21:18 eb9bd55f

View on Github →

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.

Estimated changes

Modified docs/undergrad.yaml

Created src/data/real/sign.lean

added theorem real.inv_sign

added def real.sign

added theorem real.sign_apply_eq

added theorem real.sign_inv

added theorem real.sign_mul_nonneg

added theorem real.sign_mul_pos_of_ne_zero

added theorem real.sign_neg

added theorem real.sign_of_neg

added theorem real.sign_of_not_neg

added theorem real.sign_of_zero_le

added theorem real.sign_one

added theorem real.sign_zero

Modified src/linear_algebra/quadratic_form.lean

added theorem quadratic_form.equivalent_one_neg_one_weighted_sum_squared