Integrally closed rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
An integrally closed domain
R contains all the elements of
Frac(R) that are
R. A special case of integrally closed domains are the Dedekind domains.
Main definitions #
Main results #
is_integrally_closed_iff K, where
K is a fraction field of
is integrally closed iff it is the integral closure of
R is integrally closed if all integral elements of
Frac(R) are also elements of
This definition uses
fraction_ring R to denote
if you want to choose another field of fractions for
Instances of this typeclass
R is integrally closed iff all integral elements of its fraction field
are also elements of
R is integrally closed iff it is the integral closure of itself in its field of fractions.