isIntegrallyClosed_iff — Mathlib

English

R is integrally closed iff every x in its fraction field K that is integral over R is in the image of R, i.e. there exists y ∈ R with algebraMap R K y = x.

Русский

R интегрально замкнуто тогда и только тогда, когда для любого x в поле дробей K, интегрального над R, существует y ∈ R так, что algebraMap R K y = x.

LaTeX

$$$IsIntegrallyClosed R \iff \forall x\in K\,(IsIntegral R x)\rightarrow \exists y\in R,\ algebraMap R K y = x$$$

Lean4

/-- `R` is integrally closed iff all integral elements of its fraction field `K`
are also elements of `R`. -/
theorem isIntegrallyClosed_iff : IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, algebraMap R K y = x := by
  simp [isIntegrallyClosed_iff_isIntegrallyClosedIn K, isIntegrallyClosedIn_iff, IsFractionRing.injective R K]

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