Commit 2025-05-12 07:46 0f3940c0

feat(RingTheory/LocalProperties/IntegrallyClosed): stronger version of local property of IsIntegrallyClosed (#24588) Show that an integral domain $R$ is integrally closed if there exists a set of prime ideals $S$ such that $\bigcap_{\mathfrak{p} \in S} R_{\mathfrak{p}} = R$ and for every $\mathfrak{p} \in S$, $R_{\mathfrak{p}}$ is integrally closed.