Commit 2023-06-06 13:22 e59c7618

View on Github →

feat: port LinearAlgebra.QuadraticForm.Complex (#4733)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/QuadraticForm/Complex.lean

added theorem QuadraticForm.complex_equivalent

added theorem QuadraticForm.equivalent_sum_squares