denom_div_dvd — Mathlib

English

For p, q ∈ K[X], denom(algebraMap p / algebraMap q) divides q.

Русский

Для p,q ∈ K[X] знаменатель (p/q) делит q.

LaTeX

$$$\operatorname{denom}\left(\dfrac{p}{q}\right) \mid q$$$

Lean4

@[simp]
theorem denom_div_dvd (p q : K[X]) : denom (algebraMap _ _ p / algebraMap _ _ q) ∣ q := by
  classical
  by_cases hq : q = 0
  · simp [hq]
  rw [denom_div _ hq, C_mul_dvd]
  · exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_right p q)
  · simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq

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