mathlib

e085d1df - feat(algebra/quadratic_discriminant): generalize, use `ne_zero` (#18606)

feat(algebra/quadratic_discriminant): generalize, use `ne_zero` (#18606) * Add `discrim_neg`. * Add `discrim_eq_sq_of_quadratic_eq_zero`, an implication from `quadratic_eq_zero_iff_discrim_eq_sq` that doesn't need extra assumptions. * Assume `[ne_zero (2 : _)]` instead of `2 ≠ 0` or `[invertible (2 : _)]`. * Drop unneeded assumptions in `quadratic_ne_zero_of_discrim_ne_sq`, use `s ^ 2` instead of `s * s`. * Add `discrim_le_zero_of_nonpos` and `discrim_lt_zero_of_neg`.