2026-03-26 08:33
Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
feat(RingTheory/Unramified/Dedekind): a domain finite and unramified over a Dedekind domain is a Dedekind domain (#36838) …
Added IsLocalization.AtPrime.radical_map_of_mem_minimalPrimes