The rational root theorem

The rational root theorem. If $p/q$ in lowest terms is a root of an integer polynomial, then $p$ divides the constant coefficient and $q$ divides the leading coefficient. This turns root-finding over $\mathbb{Q}$ into a finite search: only finitely many candidates need testing, so rational roots of an integer polynomial are always computable. It is also the fastest route to irrationality proofs — $\sqrt2$ is a root of $x^2 - 2$, whose only candidate rational roots are $\pm1, \pm2$, none of which work. Formalization note. num and den are the reduced numerator and denominator in the fraction field. The result is Mathlib's num_dvd_of_is_root.