scaleRoots_dvd' — Mathlib

English

If p divides q, then p.scaleRoots r divides q.scaleRoots r (under unit conditions).

Русский

Если p делит q, то p.scaleRoots r делит q.scaleRoots r (при дополнительных условиях).

LaTeX

$$$p \mid q \Rightarrow p.scaleRoots(r) \mid q.scaleRoots(r)$$$

Lean4

theorem scaleRoots_dvd' (p q : R[X]) {r : R} (hr : IsUnit r) (hpq : p ∣ q) : p.scaleRoots r ∣ q.scaleRoots r :=
  by
  obtain ⟨a, rfl⟩ := hpq
  rw [← ((hr.pow (natDegree p + natDegree a - natDegree (p * a))).map (algebraMap R R[X])).dvd_mul_left, ←
    Algebra.smul_def, mul_scaleRoots]
  exact dvd_mul_right (scaleRoots p r) (scaleRoots a r)

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