mathlib3 documentation

linear_algebra.quadratic_form.complex

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.

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

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

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

All nondegenerate quadratic forms on the complex numbers are equivalent.