isInteger_of_is_root_of_monic — Mathlib

English

Let p be a monic polynomial over a UFD A. If r in the fraction field is a root of p, there exists r' in A such that r = algebraMap A K r' and r' divides the constant term p.coeff 0.

Русский

Пусть p — моноичный полином над UFD A. Если r ∈ K является корнем p, тогда существует r' ∈ A такое, что r = algebraMap_A_K r' и r' делит константный коэффициент p.coeff 0.

LaTeX

$$$\\exists r' \\in A,\\; r = \\ algebraMap A K\\, r' \\wedge r' \\mid p(0)$$$

Lean4

/-- **Integral root theorem**:
if `r : f.codomain` is a root of a monic polynomial over the ufd `A`,
then `r` is an integer -/
theorem isInteger_of_is_root_of_monic {p : A[X]} (hp : Monic p) {r : K} (hr : aeval r p = 0) : IsInteger A r :=
  isInteger_of_isUnit_den (isUnit_of_dvd_one (hp ▸ den_dvd_of_is_root hr))

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