English
If L is a finite separable extension over Frac(A) where A is a Dedekind domain, the integral closure in L is a Dedekind domain.
Русский
Если L — конечное сепарабельноe расширение над FractionRing(A), то интегральное замыкание в L является Дедекинд доменом.
LaTeX
$$$$\\text{IsDedekindDomain}(\\text{integralClosure } A L)$$$$
Lean4
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain,
the integral closure `C` of `A` in `L` is a Dedekind domain.
This cannot be an instance since `A`, `K` or `L` can't be inferred. See also the instance
`integralClosure.isDedekindDomain_fractionRing` where `K := FractionRing A`
and `C := integralClosure A L`. -/
theorem isDedekindDomain [IsDedekindDomain A] : IsDedekindDomain C :=
have : IsFractionRing C L := IsIntegralClosure.isFractionRing_of_finite_extension A K L C
have : Algebra.IsIntegral A C := IsIntegralClosure.isIntegral_algebra A L
{ IsIntegralClosure.isNoetherianRing A K L C, Ring.DimensionLEOne.isIntegralClosure A L C,
(isIntegrallyClosed_iff L).mpr fun {x} hx =>
⟨IsIntegralClosure.mk' C x (isIntegral_trans (R := A) _ hx), IsIntegralClosure.algebraMap_mk' _ _ _⟩ with :
IsDedekindDomain C }
