Documentation

Mathlib.LinearAlgebra.QuadraticForm.Complex

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
Instances For

    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

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

      All nondegenerate quadratic forms on the complex numbers are equivalent.