# 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}
[CommRing R]
[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 : Polynomial R), p.Monic ∧ Polynomial.eval₂ f x p = 0

## Instances For

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

- IsIntegral R x = (algebraMap R A).IsIntegralElem x