Revision #3103 → #3614 · back to history
80fd593ddfcd| Field | From #3103 | To #3614 |
|---|---|---|
| mathlib.decl | Polynomial.num_dvd_of_is_root | num_dvd_of_is_root |
| note | Mathlib formalizes the rational root theorem via `num_dvd_of_is_root` and `den_dvd_of_is_root`: for a polynomial with integer coefficients, the numerator of any rational root divides the constant term and the denominator divides the leading coefficient. | Mathlib formalizes the rational root theorem via `num_dvd_of_is_root` (and `den_dvd_of_is_root`): for a polynomial over a UFD, the numerator of any root in the fraction field divides the constant coefficient and the denominator divides the leading coefficient. |
1663cfbf73c3b4cd8633d6f728642921eddf214ed27d51f3