# Integrally closed rings #

An integrally closed ring `R`

contains all the elements of `Frac(R)`

that are
integral over `R`

. A special case of integrally closed rings are the Dedekind domains.

## Main definitions #

`IsIntegrallyClosedIn R A`

states`R`

contains all integral elements of`A`

`IsIntegrallyClosed R`

states`R`

contains all integral elements of`Frac(R)`

## Main results #

`isIntegrallyClosed_iff K`

, where`K`

is a fraction field of`R`

, states`R`

is integrally closed iff it is the integral closure of`R`

in`K`

## TODO: Related notions #

The following definitions are closely related, especially in their applications in Mathlib.

A *normal domain* is a domain that is integrally closed in its field of fractions.
Stacks: normal domain
Normal domains are the major use case of `IsIntegrallyClosed`

at the time of writing, and we have
quite a few results that can be moved wholesale to a new `NormalDomain`

definition.
In fact, before PR #6126 `IsIntegrallyClosed`

was exactly defined to be a normal domain.
(So you might want to copy some of its API when you define normal domains.)

A normal ring means that localizations at all prime ideals are normal domains.
Stacks: normal ring
This implies `IsIntegrallyClosed`

,
Stacks: Tag 034M
but is equivalent to it only under some conditions (reduced + finitely many minimal primes),
Stacks: Tag 030C
in which case it's also equivalent to being a finite product of normal domains.

We'd need to add these conditions if we want exactly the products of Dedekind domains.

In fact noetherianity is sufficient to guarantee finitely many minimal primes, so `IsDedekindRing`

could be defined as `IsReduced`

, `IsNoetherian`

, `Ring.DimensionLEOne`

, and either
`IsIntegrallyClosed`

or `NormalDomain`

. If we use `NormalDomain`

then `IsReduced`

is automatic,
but we could also consider a version of `NormalDomain`

that only requires the localizations are
`IsIntegrallyClosed`

but may not be domains, and that may not equivalent to the ring itself being
`IsIntegallyClosed`

(even for noetherian rings?).

`R`

is integrally closed in `A`

if all integral elements of `A`

are also elements of `R`

.

## Equations

- IsIntegrallyClosedIn R A = IsIntegralClosure R R A

## Instances For

`R`

is integrally closed if all integral elements of `Frac(R)`

are also elements of `R`

.

This definition uses `FractionRing R`

to denote `Frac(R)`

. See `isIntegrallyClosed_iff`

if you want to choose another field of fractions for `R`

.

## Equations

## Instances For

Being integrally closed is preserved under injective algebra homomorphisms.

`R`

is integrally closed iff it is the integral closure of itself in its field of fractions.

`R`

is integrally closed iff it is the integral closure of itself in its field of fractions.

`R`

is integrally closed in `A`

iff all integral elements of `A`

are also elements of `R`

.

`R`

is integrally closed iff all integral elements of its fraction field `K`

are also elements of `R`

.

If `R`

is the integral closure of `S`

in `A`

, then it is integrally closed in `A`

.

Note that this is not a duplicate instance, since `IsIntegrallyClosed R`

is instead defined
as `IsIntegrallyClosed R R (FractionRing R)`

.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

This is almost a duplicate of `IsIntegrallyClosedIn.integralClosure_eq_bot`

,
except the `NoZeroSMulDivisors`

hypothesis isn't inferred automatically from `IsFractionRing`

.