IsIntegrallyClosedIn — Mathlib

English

Let R be a commutative ring and A an R-algebra. Then R is integrally closed in A if every element of A that is integral over R actually lies in R.

Русский

Пусть R — коммутативное кольцо и A — кольцо над R. Тогда R интегрально замкнуто в A, если каждый элемент A, являющийся интегралом над R, принадлежит R.

LaTeX

$$$IsIntegrallyClosedIn\,R\,A\;=\;IsIntegralClosure\,R\,R\,A$$$

Lean4

/-- `R` is integrally closed in `A` if all integral elements of `A` are also elements of `R`.
-/
abbrev IsIntegrallyClosedIn (R A : Type*) [CommRing R] [CommRing A] [Algebra R A] :=
  IsIntegralClosure R R A

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