Theorem IsIntegrallyClosed.of_localization_maximal

Modification history

2024-09-24 15:04

Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean

chore(Mathlib/RingTheory/LocalProperties): split LocalProperties.lean (#16879) …

Modified IsIntegrallyClosed.of_localization_maximal View on Github →

2024-09-16 11:07

Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean

feat(RingTheory/IntegralClosure/IntegrallyClosed): `IsIntegrallyClosed` is a local property (#16558) …

Added IsIntegrallyClosed.of_localization_maximal View on Github →