isDedekindDomain_fractionRing — Mathlib

English

If L is finite separable over Frac(A) and A is a Dedekind domain, the integral closure in L is a Dedekind domain.

Русский

Если L — конечное сепарабельноe расширение над FractionRing(A) и A — Дедекинд домен, то интегральное замыкание в L — Дедекинд домен.

LaTeX

$$$$\\text{IsDedekindDomain}(\\text{integralClosure } A L)$$$$

Lean4

/-- If `L` is a finite separable extension of `Frac(A)`, where `A` is a Dedekind domain,
the integral closure of `A` in `L` is a Dedekind domain.

See also the lemma `integralClosure.isDedekindDomain` where you can choose
the field of fractions yourself. -/
instance isDedekindDomain_fractionRing [IsDedekindDomain A] : IsDedekindDomain (integralClosure A L) :=
  integralClosure.isDedekindDomain A (FractionRing A) L

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