Orthonormal basis for nondegenerate symmetric bilinear

forms

For a finite-dimensional complex vector space V equipped with a symmetric nondegenerate bilinear form B, there exists an orthonormal basis — a basis b indexed by Fin (finrank ℂ V) such that B (b i) (b j) = if i = j then 1 else 0.

The proof proceeds by:

1. Using exists_orthogonal_basis (Mathlib) to obtain an orthogonal basis b₀ with B (b₀ i) (b₀ j) = 0 for i ≠ j.
2. Showing each diagonal value B (b₀ i) (b₀ i) ≠ 0 via nondegeneracy.
3. Rescaling by inverse square roots (which exist over ℂ since ℂ is algebraically closed) to normalise the diagonal entries to 1.

theorem RS.exists_orthonormal_basis {V : Type u_1} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (B : LinearMap.BilinForm ℂ V) (hsymm : ∀ (x y : V), (B x) y = (B y) x) (hnd : ∀ (x : V), (∀ (y : V), (B x) y = 0) → x = 0) : ∃ (b : Module.Basis (Fin (Module.finrank ℂ V)) ℂ V), ∀ (i j : Fin (Module.finrank ℂ V)), (B (b i)) (b j) = if i = j then 1 else 0

Orthonormal basis: a finite-dimensional complex vector space carrying a symmetric nondegenerate bilinear form admits a basis b such that B (b i) (b j) = if i = j then 1 else 0.