English
For p, q ∈ K[X] with q ≠ 0, the numerator of p/q divides p.
Русский
Пусть p, q ∈ K[X], q ≠ 0; числитель p/q делит p.
LaTeX
$$$\operatorname{num}\left(\dfrac{p}{q}\right) \mid p$, при $q \neq 0$$$
Lean4
theorem num_div_dvd (p : K[X]) {q : K[X]} (hq : q ≠ 0) : num (algebraMap _ _ p / algebraMap _ _ q) ∣ p := by
classical
rw [num_div _ q, C_mul_dvd]
· exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_left p q)
· simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq