mathlib3

93013316 - feat(algebra/cubic_discriminant): extract useful lemma from eq_sum_three_roots (#17999)