English
Let R be a commutative semiring with no zero divisors. If p divides q in R[X], then homogenize p at natDegree(p) divides homogenize q at natDegree(q).
Русский
Пусть R — коммутативное кольцо без делителей нуля. Если p делит q в R[X], то homogenize p по natDegree(p) делит homogenize q по natDegree(q).
LaTeX
$$$[NoZeroDivisors\\ R] \\, p \\mid q \\;\\Rightarrow\\; \\operatorname{homogenize}(p, p.natDegree) \\mid \\operatorname{homogenize}(q, q.natDegree).$$$
Lean4
theorem homogenize_dvd [NoZeroDivisors R] {p q : R[X]} (h : p ∣ q) :
homogenize p p.natDegree ∣ homogenize q q.natDegree :=
by
rcases h with ⟨r, rfl⟩
obtain rfl | rfl | ⟨hp₀, hr₀⟩ : p = 0 ∨ r = 0 ∨ p ≠ 0 ∧ r ≠ 0 := by tauto
· simp
· simp
· rw [natDegree_mul hp₀ hr₀, homogenize_mul _ _ le_rfl le_rfl]
apply dvd_mul_right
