isIntegrallyClosed_iff_isIntegrallyClosedIn

English

R is integrally closed if and only if it is the integral closure of itself in its field of fractions K.

Русский

R интегрально замкнуто тогда и только тогда, когда R является своей интегральной замкнутостью в своем поле дробей K.

LaTeX

$$$IsIntegrallyClosed R \iff IsIntegrallyClosedIn R\;K$$$

Lean4

/-- `R` is integrally closed iff it is the integral closure of itself in its field of fractions. -/
theorem isIntegrallyClosed_iff_isIntegrallyClosedIn : IsIntegrallyClosed R ↔ IsIntegrallyClosedIn R K :=
  (IsLocalization.algEquiv R⁰ _ _).isIntegrallyClosedIn

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