Commit 2024-09-16 11:07 d389f3c5

View on Github →

feat(RingTheory/IntegralClosure/IntegrallyClosed): IsIntegrallyClosed is a local property (#16558) Prove that IsIntegrallyClosed is a local property, i.e., an integral domain R is integral closed if Rₘ is integral closed for any maximal ideal m of R.

Estimated changes

Modified Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean

added theorem IsIntegrallyClosed.of_localization_maximal

Modified Mathlib/RingTheory/LocalProperties.lean

added theorem isIntegrallyClosed_ofLocalizationMaximal

Modified Mathlib/RingTheory/Localization/Basic.lean

added theorem IsLocalization.eq_mk'_of_mul_eq

Modified Mathlib/RingTheory/Localization/LocalizationLocalization.lean

added theorem IsLocalization.mk'_eq_algebraMap_mk'_of_submonoid_le