Commit 2024-02-14 08:30 30c9985e

View on Github →

feat: an irreducible real polynomial has degree ≤2 (#10431)

Estimated changes

Modified Mathlib/Analysis/Complex/Polynomial.lean

added theorem Irreducible.degree_le_two

added theorem Irreducible.nat_degree_le_two

added theorem Polynomial.mul_star_dvd_of_aeval_eq_zero_im_ne_zero

added theorem Polynomial.quadratic_dvd_of_aeval_eq_zero_im_ne_zero

Modified Mathlib/Data/IsROrC/Lemmas.lean

added theorem Polynomial.aeval_conj

added theorem Polynomial.aeval_ofReal