English
Let A be a Dedekind domain and L a finite separable extension; then the integral closure of A in L is Dedekind even after passing to FractionRing A.
Русский
Пусть A — Дедекинд домен и L — конечное сепарабельноe расширение; интегральное замыкание A в L остается Дедекинд доменом после перехода к FractionRing A.
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 of `A` in `L` is a Dedekind domain.
This cannot be an instance since `K` can't be inferred. See also the instance
`integralClosure.isDedekindDomain_fractionRing` where `K := FractionRing A`. -/
theorem isDedekindDomain [IsDedekindDomain A] : IsDedekindDomain (integralClosure A L) :=
IsIntegralClosure.isDedekindDomain A K L (integralClosure A L)
