of_aeval_monic — Mathlib

English

If a monic polynomial p over R evaluated at x is integral and deg p > 0, then x is integral.

Русский

Если моноциклический многочлен p над R в точке x образует интегральный элемент и deg p > 0, то x интегрален.

LaTeX

$$$\\text{Monic}(p)\\land p.natDegree \\neq 0\\ \\land\\ \\text{IsIntegral}_R(\\operatorname{aeval}_x p) \\Rightarrow \\text{IsIntegral}_R(x)$$$

Lean4

theorem of_aeval_monic {x : A} {p : R[X]} (monic : p.Monic) (deg : p.natDegree ≠ 0) (hx : IsIntegral R (aeval x p)) :
    IsIntegral R x :=
  have ⟨p, hmonic, heval⟩ := hx
  ⟨_, hmonic.comp monic deg, by rwa [eval₂_comp, ← aeval_def x]⟩

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