degree_le_of_ne_zero — Mathlib

English

In an integrally closed domain, the minimal polynomial is uniquely determined by its root property.

Русский

В интегрально закрытом домене минимальный полином уникально определяется своей корневой характеристикой.

LaTeX

$$$\text{IsIntegrallyClosed.minpoly.unique}$$$

Lean4

/-- If an element `x` is a root of a nonzero polynomial `p`, then the degree of `p` is at least the
degree of the minimal polynomial of `x`. See also `minpoly.degree_le_of_ne_zero` which relaxes the
assumptions on `S` in exchange for stronger assumptions on `R`. -/
theorem degree_le_of_ne_zero {s : S} (hs : IsIntegral R s) {p : R[X]} (hp0 : p ≠ 0) (hp : Polynomial.aeval s p = 0) :
    degree (minpoly R s) ≤ degree p :=
  by
  rw [degree_eq_natDegree (minpoly.ne_zero hs), degree_eq_natDegree hp0]
  norm_cast
  exact natDegree_le_of_dvd ((isIntegrallyClosed_dvd_iff hs _).mp hp) hp0

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