isNoetherianRing — Mathlib

English

If L is a finite separable extension of K = Frac(A) with A Dedekind domain, the integral closure C of A in L is a Dedekind domain.

Русский

Если L — конечное сепарабельноe расширение K = 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
integrally closed and Noetherian, the integral closure of `A` in `L` is
Noetherian. -/
theorem isNoetherianRing [IsIntegrallyClosed A] [IsNoetherianRing A] : IsNoetherianRing (integralClosure A L) :=
  IsIntegralClosure.isNoetherianRing A K L (integralClosure A L)

Похожие утверждения