# mathlibdocumentation

ring_theory.integrally_closed

# Integrally closed rings #

An integrally closed domain R contains all the elements of Frac(R) that are integral over R. A special case of integrally closed domains are the Dedekind domains.

## Main definitions #

• is_integrally_closed R states R contains all integral elements of Frac(R)

## Main results #

• is_integrally_closed_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]
structure is_integrally_closed (R : Type u_1) [comm_ring R] [is_domain R] :
Prop
• algebra_map_eq_of_integral : ∀ {x : , x(∃ (y : R), (fraction_ring R)) y = x)

R is integrally closed if all integral elements of Frac(R) are also elements of R.

This definition uses fraction_ring R to denote Frac(R). See is_integrally_closed_iff if you want to choose another field of fractions for R.

Instances of this typeclass
theorem is_integrally_closed_iff {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K] :
∀ {x : K}, x(∃ (y : R), K) y = x)

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

theorem is_integrally_closed_iff_is_integral_closure {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K] :

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

@[protected, instance]
def is_integrally_closed.is_integral_closure {R : Type u_1} [comm_ring R] [is_domain R] [iic : is_integrally_closed R] {K : Type u_2} [field K] [ K] [ K] :
K
theorem is_integrally_closed.is_integral_iff {R : Type u_1} [comm_ring R] [is_domain R] [iic : is_integrally_closed R] {K : Type u_2} [field K] [ K] [ K] {x : K} :
x ∃ (y : R), K) y = x
theorem is_integrally_closed.integral_closure_eq_bot_iff {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K] :
@[simp]
theorem is_integrally_closed.integral_closure_eq_bot (R : Type u_1) [comm_ring R] [is_domain R] [iic : is_integrally_closed R] (K : Type u_2) [field K] [ K] [ K] :
theorem integral_closure.is_integrally_closed_of_finite_extension {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K] {L : Type u_3} [field L] [ L] [ L] [ L] [ L] :