Theorem quadratic_form.equivalent_weighted_sum_squares_units_of_nondegenerate'
Modification history
2022-05-24 10:24
src/linear_algebra/quadratic_form/basic.lean
feat(linear_algebra/quadratic_form/isometry): extract from `linear_algebra/quadratic_form/basic` (#14305) …
Modified quadratic_form.equivalent_weighted_sum_squares_units_of_nondegenerate'View on Github →2021-10-01 10:38
src/linear_algebra/quadratic_form.lean
feat(linear_algebra/{bilinear,quadratic}_form): remove non-degeneracy requirement from `exists_orthogonal_basis` and Sylvester's law of inertia (#9465) …
Added quadratic_form.equivalent_weighted_sum_squares_units_of_nondegenerate'View on Github →