associated_of_dvd_of_degree_eq — Mathlib

English

If p ∣ q and deg(p) = deg(q) for polynomials over a field, then p and q are associated.

Русский

Если p делит q и deg(p) = deg(q) для многочленов над полем, то p и q ассоциированы.

LaTeX

$$$p \mid q \land \deg(p) = \deg(q) \Rightarrow Associated(p,q).$$$

Lean4

theorem associated_of_dvd_of_degree_eq {K} [Field K] {p q : K[X]} (hpq : p ∣ q) (h₁ : p.degree = q.degree) :
    Associated p q :=
  (Classical.em (q = 0)).elim (fun hq ↦ (show p = q by simpa [hq] using h₁) ▸ Associated.refl p)
    (associated_of_dvd_of_natDegree_le hpq · (natDegree_le_natDegree h₁.ge))

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