theorem Polynomial.eval_and_derivative_eval_eq_zero_iff {R : Type u_1} [CommRing R] (f : Polynomial R) (a : R) : eval a f = 0 ∧ eval a (derivative f) = 0 ↔ ∃ (g : Polynomial R), f = (X - C a) ^ 2 * g