IsIntegrallyClosed is a local property

In this file, we prove that IsIntegrallyClosed is a local property.

Main results

• IsIntegrallyClosed.of_localization_maximal : An integral domain R is integral closed if Rₘ is integral closed for any maximal ideal m of R.

TODO

Prove that IsIntegrallyClosed is preserved by localization

theorem IsIntegrallyClosed.of_localization_maximal {R : Type u_1} [CommRing R] [IsDomain R] (h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)) : IsIntegrallyClosed R

An integral domain R is integral closed if Rₘ is integral closed for any maximal ideal m of R.

theorem isIntegrallyClosed_ofLocalizationMaximal : OfLocalizationMaximal fun (R : Type u_1) (x : CommRing R) => ∀ [inst : IsDomain R], IsIntegrallyClosed R