integralClosure_eq_bot_iff — Mathlib

English

IsIntegrallyClosed in R is equivalent to integralClosure R K equals the bottom, i.e. R is integrally closed iff the integral closure in K is R.

Русский

IsIntegrallyClosed в R эквивалентно тому, что integralClosure R K равна нижнему; то есть R интегрально замкнуто тогда и только тогда, когда интегральное замыкание в K равно R.

LaTeX

$$$IsIntegrallyClosed R \iff IsIntegralClosure R R K$ (equivalence with isIntegrallyClosedIn).$$

Lean4

theorem integralClosure_eq_bot_iff : integralClosure R K = ⊥ ↔ IsIntegrallyClosed R :=
  (IsIntegrallyClosedIn.integralClosure_eq_bot_iff _ (IsFractionRing.injective _ _)).trans
    (isIntegrallyClosed_iff_isIntegrallyClosedIn _).symm

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