mathlib documentation

linear_algebra.quadratic_form.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 quadratic_form.isometry_sum_squares {ι : 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 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.