Commit 2023-06-06 22:12 2076bf0f

View on Github →

feat: port LinearAlgebra.QuadraticForm.Real (#4758)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/QuadraticForm/Real.lean

added theorem QuadraticForm.equivalent_one_neg_one_weighted_sum_squared

added theorem QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared