theorem BilinearForms.bilinearForm_matrix_correspondence {n : ℕ} (B : LinearMap.BilinForm ℝ (Fin n → ℝ)) : (∃ (A : Matrix (Fin n) (Fin n) ℝ), Matrix.toBilin' A = B) ∧ (LinearMap.IsSymm B ↔ (LinearMap.BilinForm.toMatrix' B).IsSymm)

theorem BilinearForms.orthogonal_complement_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (W : Submodule R M) (v : M) : v ∈ B.orthogonal W ↔ ∀ w ∈ W, B.IsOrtho w v

theorem BilinearForms.nondegenerate_iff_det_ne_zero {A : Type u_1} [CommRing A] [IsDomain A] {M : Type u_2} [AddCommGroup M] [Module A M] {ι : Type u_3} [DecidableEq ι] [Fintype ι] (B : LinearMap.BilinForm A M) (b : Module.Basis ι A M) : B.Nondegenerate ↔ ((LinearMap.BilinForm.toMatrix b) B).det ≠ 0

theorem BilinearForms.exists_normalized_orthogonal_basis {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) : ∃ (w : Fin (Module.finrank ℝ M) → ℝ), (∀ (i : Fin (Module.finrank ℝ M)), w i = -1 ∨ w i = 0 ∨ w i = 1) ∧ QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ w)

theorem BilinearForms.signature_invariance {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q Q' : QuadraticForm ℝ M} (h : QuadraticMap.Equivalent Q Q') : sigPos Q = sigPos Q' ∧ sigNeg Q = sigNeg Q' ∧ Module.finrank ℝ M - sigPos Q - sigNeg Q = Module.finrank ℝ M - sigPos Q' - sigNeg Q'