Theorems · Theorem · commutative algebra

IsIntegrallyClosed.of_isLocalization_maximal

∀ {R : Type u_1} [inst : CommRing R] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3)
  [inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)]
  [inst_2 : (P : Ideal R) → [inst_2 : P.IsMaximal] → Algebra R (Rₚ P)]
  [∀ (P : Ideal R) [inst_3 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] [IsDomain R],
  (∀ (P : Ideal R) [inst : P.IsMaximal], IsIntegrallyClosed (Rₚ P)) → IsIntegrallyClosed R

Defined in

Mathlib.RingTheory.LocalProperties.IntegrallyClosed

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsLocalization.AtPrimeIsDomain