English
A nondegenerate quadratic form on a complex finite-dimensional space is equivalent to the sum of squares, i.e., toWeightedSumSquares with all weights equal to 1.
Русский
Nondegenerate квадратичная форма на комплексном конечномерном пространстве эквивалентна сумме квадратов, т.е. WeightedSumSquares ℂ с весами 1(для всех компонент).
LaTeX
$$$ Q \\text{ nondegenerate} \\Rightarrow Q \\sim weightedSumSquares\\ ℂ (1) $$$
Lean4
/-- A nondegenerate quadratic form on the complex numbers is equivalent to
the sum of squares, i.e. `weightedSumSquares` with weight `fun (i : ι) => 1`. -/
theorem equivalent_sum_squares {M : Type*} [AddCommGroup M] [Module ℂ M] [FiniteDimensional ℂ M] (Q : QuadraticForm ℂ M)
(hQ : (associated (R := ℂ) Q).SeparatingLeft) :
Equivalent Q (weightedSumSquares ℂ (1 : Fin (Module.finrank ℂ M) → ℂ)) :=
let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares_units_of_nondegenerate' hQ
⟨hw₁.trans (isometryEquivSumSquaresUnits w)⟩
