associated_of_dvd_of_natDegree_le

English

Let K be a field and p, q ∈ K[X] with hpq : p ∣ q, hq : q ≠ 0, and h₁ : q.natDegree ≤ p.natDegree. Then p and q are associated.

Русский

Пусть K — поле, и p, q ∈ K[X] такие, что p делит q, q ≠ 0, и q.natDegree ≤ p.natDegree. Тогда p и q ассоциированы.

LaTeX

$$$p \mid q \land q \ne 0 \land q.natDegree \le p.natDegree \Rightarrow Associated(p,q).$$$

Lean4

theorem associated_of_dvd_of_natDegree_le {K} [Field K] {p q : K[X]} (hpq : p ∣ q) (hq : q ≠ 0)
    (h₁ : q.natDegree ≤ p.natDegree) : Associated p q :=
  associated_of_dvd_of_natDegree_le_of_leadingCoeff hpq h₁
    (IsUnit.dvd (by rwa [← leadingCoeff_ne_zero, ← isUnit_iff_ne_zero] at hq))

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