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} [Fintype ι] (w' : ι → ℂ) : (QuadraticMap.weightedSumSquares ℂ w').IsometryEquiv (QuadraticMap.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

• QuadraticForm.isometryEquivSumSquares w' = ⋯.mpr ((QuadraticMap.weightedSumSquares ℂ w').isometryEquivBasisRepr ((Pi.basisFun ℂ ι).unitsSMul fun (i : ι) => ⋯.unit))

noncomputable def QuadraticForm.isometryEquivSumSquaresUnits {ι : Type u_1} [Fintype ι] (w : ι → ℂˣ) : (QuadraticMap.weightedSumSquares ℂ w).IsometryEquiv (QuadraticMap.weightedSumSquares ℂ 1)

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

• QuadraticForm.isometryEquivSumSquaresUnits w = ⋯.mp (QuadraticForm.isometryEquivSumSquares (Units.val ∘ w))

theorem QuadraticForm.equivalent_sum_squares {M : Type u_2} [AddCommGroup M] [Module ℂ M] [FiniteDimensional ℂ M] (Q : QuadraticForm ℂ M) (hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)) : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℂ 1)

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} [AddCommGroup M] [Module ℂ M] [FiniteDimensional ℂ M] (Q₁ Q₂ : QuadraticForm ℂ M) (hQ₁ : LinearMap.SeparatingLeft (QuadraticMap.associated Q₁)) (hQ₂ : LinearMap.SeparatingLeft (QuadraticMap.associated Q₂)) : QuadraticMap.Equivalent Q₁ Q₂

All nondegenerate quadratic forms on the complex numbers are equivalent.