isIntegral — Mathlib

English

If x is integral over R and y is a conjugate root of x over R, then y is also integral over R.

Русский

Если x интегральен над R и y является сопряжённым корнем x над R, то y также интегрально над R.

LaTeX

$$$\text{IsIntegral }(R,x) \;\land\; \text{IsConjRoot }(R,x,y) \Rightarrow \text{IsIntegral }(R,y)$$$

Lean4

/-- If `y` is a conjugate root of an integral element `x` over `R`, then `y` is also integral
over `R`.
-/
theorem isIntegral {x y : A} (hx : IsIntegral R x) (h : IsConjRoot R x y) : IsIntegral R y :=
  ⟨minpoly R x, minpoly.monic hx, h ▸ minpoly.aeval R y⟩

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