isIntegrallyClosed_ofLocalizationMaximal

English

If there is a family of localized rings at maximal ideals, each integrally closed, then the original ring is integrally closed.

Русский

Если существует семейство локализаций по максимальным идеалам, каждая из которых интегрально замкнута, то исходное кольцо интегрально замкнуто.

LaTeX

$$$\\forall P \\text{ maximal}, IsIntegrallyClosed(R_p) \\Rightarrow IsIntegrallyClosed(R).$$$

Lean4

theorem isIntegrallyClosed_ofLocalizationMaximal :
    OfLocalizationMaximal fun R _ => ([IsDomain R] → IsIntegrallyClosed R) := fun _ _ h _ ↦
  IsIntegrallyClosed.of_localization_maximal fun p _ hpm ↦ h p hpm

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