Commit 2021-06-07 15:40 fa7b5f20

View on Github →

feat(linear_algebra/quadratic_form): Complex version of Sylvester's law of inertia (#7416) Every nondegenerate complex quadratic form is equivalent to a quadratic form corresponding to the sum of squares.

Estimated changes

Modified src/linear_algebra/basis.lean

added def basis.group_smul

added theorem basis.group_smul_apply

added theorem basis.group_smul_span_eq_top

added def basis.is_unit_smul

added theorem basis.is_unit_smul_apply

added def basis.units_smul

added theorem basis.units_smul_apply

added theorem basis.units_smul_span_eq_top

Modified src/linear_algebra/clifford_algebra/basic.lean

Modified src/linear_algebra/linear_independent.lean

added theorem linear_independent.group_smul

added theorem linear_independent.units_smul

Modified src/linear_algebra/quadratic_form.lean

added theorem quadratic_form.basis_repr_apply

added theorem quadratic_form.equivalent_sum_squares

added theorem quadratic_form.equivalent_weighted_sum_squares_of_nondegenerate'

added def quadratic_form.isometry_of_comp_linear_equiv

added theorem quadratic_form.isometry_of_is_Ortho_apply

added def quadratic_form.weighted_sum_squares

added theorem quadratic_form.weighted_sum_squares_apply