isIntegrallyClosedOfFiniteExtension

English

Let R be a domain and L a finite extension of its fraction field K. The integral closure of R in L is integrally closed.

Русский

Пусть R — области, а L — конечное расширение многочленного поля K. Интегральное замыкание R в L является интегрально замкнутым.

LaTeX

$$$\\text{IsIntegrallyClosed}(\operatorname{integralClosure}(R,L))$$$

Lean4

theorem isIntegrallyClosedOfFiniteExtension [IsDomain R] [FiniteDimensional K L] :
    IsIntegrallyClosed (integralClosure R L) :=
  letI : IsFractionRing (integralClosure R L) L := isFractionRing_of_finite_extension K L
  (integralClosure_eq_bot_iff L).mp integralClosure_idem

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