Theorem Polynomial.quadratic_dvd_of_aeval_eq_zero_im_ne_zero

Modification history

2024-02-14 08:30
Mathlib/Analysis/Complex/Polynomial.lean
feat: an irreducible real polynomial has degree ≤2 (#10431)
Added Polynomial.quadratic_dvd_of_aeval_eq_zero_im_ne_zeroView on Github →