# 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' : ι) :
.IsometryEquiv (QuadraticForm.weightedSumSquares fun (i : ι) => if w' i = 0 then 0 else 1)

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def QuadraticForm.isometryEquivSumSquaresUnits {ι : Type u_1} [] (w : ι) :
.IsometryEquiv

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.

Equations
Instances For
theorem QuadraticForm.equivalent_sum_squares {M : Type u_2} [] [] [] (Q : ) (hQ : LinearMap.SeparatingLeft (QuadraticForm.associated Q)) :
Q.Equivalent

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₁ : LinearMap.SeparatingLeft (QuadraticForm.associated Q₁)) (hQ₂ : LinearMap.SeparatingLeft (QuadraticForm.associated Q₂)) :
Q₁.Equivalent Q₂

All nondegenerate quadratic forms on the complex numbers are equivalent.