Theorem QuadraticForm.equivalent_sign_ne_zero_weighted_sum_squared

Modification history

2024-04-24 13:42
Mathlib/LinearAlgebra/QuadraticForm/Real.lean
refactor(QuadraticForm/Real): migrate to `SignType` (#12319) …
Added QuadraticForm.equivalent_sign_ne_zero_weighted_sum_squaredView on Github →