English
Let R be a commutative ring and A an R-algebra. The integral closure of R in A is the subalgebra of A consisting exactly of those elements that are integral over R; in particular it contains the image of R and is closed under addition and multiplication.
Русский
Пусть R — коммутативное кольцо, A — R-алгебра. Интегральное замыкание R в A есть подалгебра A, состоящая из элементов, которые интегральны над R; в частности, изображение R лежит в этом подкольце и оно замкнуто относительно сложения и умножения.
LaTeX
$$$\operatorname{integralClosure}(R,A) = \{ a \in A \mid \IsIntegral(R,a) \}$ как подалгебра над R в A$$
Lean4
/-- The integral closure of `R` in an `R`-algebra `A`. -/
def integralClosure : Subalgebra R A where
carrier := {r | IsIntegral R r}
zero_mem' := isIntegral_zero
one_mem' := isIntegral_one
add_mem' := IsIntegral.add
mul_mem' := IsIntegral.mul
algebraMap_mem' _ := isIntegral_algebraMap
