# Documentation

Mathlib.RingTheory.IntegrallyClosed

# 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 #

• 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
class IsIntegrallyClosed (R : Type u_1) [] :
• algebraMap_eq_of_integral : ∀ {x : }, y, ↑() y = x

All integral elements of Frac(R) are also elements of R.

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.

Instances
theorem isIntegrallyClosed_iff {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] :
∀ {x : K}, y, ↑() y = x

R is integrally closed iff all integral elements of its fraction field K are also elements of R.

theorem isIntegrallyClosed_iff_isIntegralClosure {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] :

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

instance IsIntegrallyClosed.instIsIntegralClosureToCommSemiring {R : Type u_1} [] [iic : ] {K : Type u_2} [] [Algebra R K] [ifr : ] :
theorem IsIntegrallyClosed.isIntegral_iff {R : Type u_1} [] [iic : ] {K : Type u_2} [] [Algebra R K] [ifr : ] {x : K} :
y, ↑() y = x
theorem IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow {R : Type u_1} [] [iic : ] {K : Type u_2} [] [Algebra R K] [ifr : ] {x : K} {n : } (hn : 0 < n) (hx : IsIntegral R (x ^ n)) :
y, ↑() y = x
theorem IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebra {R : Type u_1} [] {K : Type u_3} [] [Algebra R K] {S : } [IsIntegrallyClosed { x // x S }] [IsFractionRing { x // x S } K] {x : K} {n : } (hn : 0 < n) (hx : x ^ n S) :
y, ↑(algebraMap { x // x S } K) y = x
theorem IsIntegrallyClosed.integralClosure_eq_bot_iff {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [ifr : ] :
@[simp]
theorem IsIntegrallyClosed.integralClosure_eq_bot (R : Type u_1) [] [iic : ] (K : Type u_2) [] [Algebra R K] [ifr : ] :
theorem integralClosure.isIntegrallyClosedOfFiniteExtension {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] {L : Type u_3} [] [Algebra K L] [Algebra R L] [] [] [] :