Commit 2021-10-01 10:38 265345c2

feat(linear_algebra/{bilinear,quadratic}_form): remove non-degeneracy requirement from exists_orthogonal_basis and Sylvester's law of inertia (#9465) This removes the nondegenerate hypothesis from bilin_form.exists_orthogonal_basis, and removes the ∀ i, B (v i) (v i) ≠ 0 statement from the goal. This property can be recovered in the case of a nondegenerate form with is_Ortho.not_is_ortho_basis_self_of_nondegenerate. This also swaps the order of the binders in is_Ortho to make it expressible with pairwise.