Commit 2023-03-18 04:16 e085d1df

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.