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' : ι → Complex)
:
(QuadraticMap.weightedSumSquares Complex w').IsometryEquiv
(QuadraticMap.weightedSumSquares Complex fun (i : ι) => ite (Eq (w' i) 0) 0 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
- Eq (QuadraticForm.isometryEquivSumSquares w') (⋯.mpr ((QuadraticMap.weightedSumSquares Complex w').isometryEquivBasisRepr ((Pi.basisFun Complex ι).unitsSMul fun (i : ι) => ⋯.unit)))
Instances For
noncomputable def
QuadraticForm.isometryEquivSumSquaresUnits
{ι : Type u_1}
[Fintype ι]
(w : ι → Units Complex)
:
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}
[AddCommGroup M]
[Module Complex M]
[FiniteDimensional Complex M]
(Q : QuadraticForm Complex M)
(hQ : LinearMap.SeparatingLeft (DFunLike.coe QuadraticMap.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}
[AddCommGroup M]
[Module Complex M]
[FiniteDimensional Complex M]
(Q₁ Q₂ : QuadraticForm Complex M)
(hQ₁ : LinearMap.SeparatingLeft (DFunLike.coe QuadraticMap.associated Q₁))
(hQ₂ : LinearMap.SeparatingLeft (DFunLike.coe QuadraticMap.associated Q₂))
:
QuadraticMap.Equivalent Q₁ Q₂
All nondegenerate quadratic forms on the complex numbers are equivalent.