mathlib3
32d1dfcb - feat(linear_algebra/quadratic_form): nondegenerate quadratic forms (#5045)

Commit

5 years ago

feat(linear_algebra/quadratic_form): nondegenerate quadratic forms (#5045) No real lemmas about these, but `nondegenerate Q` is easier to read than `∀ x, Q x = 0 → x = 0`

Author

eric-wieser

Parents

8d40e8d0

mathlib3 32d1dfcb - feat(linear_algebra/quadratic_form): nondegenerate quadratic forms (#5045)

mathlib3
32d1dfcb - feat(linear_algebra/quadratic_form): nondegenerate quadratic forms (#5045)