Quadratic forms over the complex numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

noncomputable def quadratic_form.isometry_sum_squares {ι : Type u_1} [fintype ι] [decidable_eq ι] (w' : ι ) :
(λ (i : ι), ite (w' i = 0) 0 1))

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

Equations
noncomputable def quadratic_form.isometry_sum_squares_units {ι : Type u_1} [fintype ι] [decidable_eq ι] (w : ι ˣ) :

The isometry between a weighted sum of squares on the complex numbers and the sum of squares, i.e. weighted_sum_squares with weight λ i : ι, 1.

Equations
theorem quadratic_form.equivalent_sum_squares {M : Type u_1} [ M] (Q : M) (hQ : .nondegenerate) :

A nondegenerate quadratic form on the complex numbers is equivalent to the sum of squares, i.e. weighted_sum_squares with weight λ i : ι, 1.

theorem quadratic_form.complex_equivalent {M : Type u_1} [ M] (Q₁ Q₂ : M) (hQ₁ : .nondegenerate) (hQ₂ : .nondegenerate) :
Q₁.equivalent Q₂

All nondegenerate quadratic forms on the complex numbers are equivalent.