Commit 2024-04-24 13:42 b53e4a35

View on Github →

refactor(QuadraticForm/Real): migrate to SignType (#12319) See also #7842

Estimated changes

Modified Mathlib/Data/Sign.lean

added theorem self_mul_sign

added theorem sign_mul_self

Modified Mathlib/LinearAlgebra/QuadraticForm/Real.lean

added theorem QuadraticForm.equivalent_signType_weighted_sum_squared

added theorem QuadraticForm.equivalent_sign_ne_zero_weighted_sum_squared