English
If L is a finite separable extension of Frac(A) with A a Dedekind domain, and C is the integral closure of A in L, then C is a Dedekind domain.
Русский
Пусть L — конечное сепарабельноe расширение Frac(A) с A — Дедекинд домен. Интегральное замыкание C A в L является Дедекинд доменом.
LaTeX
$$$$\\text{IsDedekindDomain}(C)$$$$
Lean4
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a principal ring
and `L` has no zero smul divisors by `A`, the integral closure `C` of `A` in `L` is
a free `A`-module. -/
theorem module_free [NoZeroSMulDivisors A L] [IsPrincipalIdealRing A] : Module.Free A C :=
haveI : NoZeroSMulDivisors A C := IsIntegralClosure.noZeroSMulDivisors A L
haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L _
inferInstance
