num_div_dvd — Mathlib

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

Похожие утверждения