# Integral closure of a subring. #

If A is an R-algebra then a : A is integral over R if it is a root of a monic polynomial with coefficients in R.

## Main definitions #

Let R be a CommRing and let A be an R-algebra.

• RingHom.IsIntegralElem (f : R →+* A) (x : A) : x is integral with respect to the map f,

• IsIntegral (x : A) : x is integral over R, i.e., is a root of a monic polynomial with coefficients in R.

def RingHom.IsIntegralElem {R : Type u_1} {A : Type u_3} [] [Ring A] (f : R →+* A) (x : A) :

An element x of A is said to be integral over R with respect to f if it is a root of a monic polynomial p : R[X] evaluated under f

Equations
• f.IsIntegralElem x = ∃ (p : ), p.Monic = 0
Instances For
def RingHom.IsIntegral {R : Type u_1} {A : Type u_3} [] [Ring A] (f : R →+* A) :

A ring homomorphism f : R →+* A is said to be integral if every element A is integral with respect to the map f

Equations
• f.IsIntegral = ∀ (x : A), f.IsIntegralElem x
Instances For
def IsIntegral (R : Type u_1) {A : Type u_3} [] [Ring A] [Algebra R A] (x : A) :

An element x of an algebra A over a commutative ring R is said to be integral, if it is a root of some monic polynomial p : R[X]. Equivalently, the element is integral over R with respect to the induced algebraMap

Equations
Instances For