English
Let p, q be polynomials over a domain with hpq : p ∣ q, h₁ : q.natDegree ≤ p.natDegree, and h₂ : q.leadingCoeff ∣ p.leadingCoeff. Then p and q are associated; i.e., there exists a unit u with p = u q.
Русский
Пусть p, q — многочлены над областью, p делит q, q.natDegree ≤ p.natDegree и q.leadingCoeff делит p.leadingCoeff. Тогда p и q ассоциированы; существует единица u такая, что p = u q.
LaTeX
$$$p \mid q \;\land\; q.natDegree \le p.natDegree \;\land\; q.leadingCoeff \mid p.leadingCoeff \Rightarrow \exists u \in R^{\times},\ p = u \cdot q.$$$
Lean4
theorem associated_of_dvd_of_natDegree_le_of_leadingCoeff {p q : R[X]} (hpq : p ∣ q) (h₁ : q.natDegree ≤ p.natDegree)
(h₂ : q.leadingCoeff ∣ p.leadingCoeff) : Associated p q :=
have ⟨r, hr⟩ := hpq
have ⟨u, hu⟩ := associated_of_dvd_dvd ⟨leadingCoeff r, hr ▸ leadingCoeff_mul p r⟩ h₂
⟨Units.map C.toMonoidHom u,
eq_of_dvd_of_natDegree_le_of_leadingCoeff (by rwa [Units.mul_right_dvd]) (by simpa [natDegree_mul_C] using h₁)
(by simpa using hu)⟩
