Theorems · Theorem · commutative algebra

isIntegrallyClosed_iff

∀ {R : Type u_1} [inst : CommRing R] (K : Type u_4) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, (algebraMap R K) y = x

R is integrally closed iff all integral elements of its fraction field K are also elements of R.

Defined in

Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Cited by

10 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraIsFractionRing