scaleRoots_dvd_iff — Mathlib

English

Let R be a commutative semiring. For polynomials p, q ∈ R[X] and a unit r ∈ R, p.scaleRoots(r) divides q.scaleRoots(r) if and only if p divides q.

Русский

Пусть R — коммутативная полукольца. Пусть p, q ∈ R[X] и r ∈ R является единицей; тогда p.scaleRoots(r) делит q.scaleRoots(r) тогда и только тогда, когда p делит q.

LaTeX

$$$\\forall R [\\mathrm{CommSemiring}\\ R] (p,q \\in R[X]) (r \\in R) (hr : R^\\times),\\; p.scaleRoots(r) \\mid q.scaleRoots(r) \\;\\iff\\; p \\mid q$$$

Lean4

theorem scaleRoots_dvd_iff (p q : R[X]) {r : R} (hr : IsUnit r) : p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q :=
  by
  refine ⟨?_ ∘ scaleRoots_dvd' _ _ (hr.unit⁻¹).isUnit, scaleRoots_dvd' p q hr⟩
  simp [← scaleRoots_mul, scaleRoots_one]

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