# Quadratic forms over the complex numbers #

equivalent_sum_squares: A nondegenerate quadratic form over the complex numbers is equivalent to a sum of squares.

noncomputable def QuadraticForm.isometryEquivSumSquares {ι : Type u_1} [] [] (w' : ι) :

The isometry between a weighted sum of squares on the complex numbers and the sum of squares, i.e. weightedSumSquares with weights 1 or 0.

Instances For
noncomputable def QuadraticForm.isometryEquivSumSquaresUnits {ι : Type u_1} [] [] (w : ι) :

The isometry between a weighted sum of squares on the complex numbers and the sum of squares, i.e. weightedSumSquares with weight fun (i : ι) => 1.

Instances For
theorem QuadraticForm.equivalent_sum_squares {M : Type u_2} [] [] [] (Q : ) (hQ : BilinForm.Nondegenerate (QuadraticForm.associated Q)) :

A nondegenerate quadratic form on the complex numbers is equivalent to the sum of squares, i.e. weightedSumSquares with weight fun (i : ι) => 1.

theorem QuadraticForm.complex_equivalent {M : Type u_2} [] [] [] (Q₁ : ) (Q₂ : ) (hQ₁ : BilinForm.Nondegenerate (QuadraticForm.associated Q₁)) (hQ₂ : BilinForm.Nondegenerate (QuadraticForm.associated Q₂)) :

All nondegenerate quadratic forms on the complex numbers are equivalent.