Commit 2024-04-11 07:48 37c70acc

refactor(RingTheory/IntegrallyClosed): generalize to IsIntegrallyClosedIn (#7857) This refactor adds a new definition IsIntegrallyClosedIn R A equal to IsIntegralClosure R A A, and redefines IsIntegrallyClosed R to equal IsIntegrallyClosed R (FractionRing A). This should make it possible and convenient to generalize away from the fraction fields. This also more closely approximates the conventions of the Stacks project. This is a second attempt at the refactor, after #7116 which was much more messy.