mathlib

c1d80c11 - feat(algebra/cubic_discriminant): add eq_zero and ne_zero lemmas (#17627)

feat(algebra/cubic_discriminant): add eq_zero and ne_zero lemmas (#17627) E.g. to allow `degree_of_c_eq_zero'` instead of `degree_of_c_eq_zero rfl rfl rfl` when the cubic is known to be constant.