Commit 2026-03-26 08:33 eef638e7

View on Github →

feat(RingTheory/Unramified/Dedekind): a domain finite and unramified over a Dedekind domain is a Dedekind domain (#36838) This PR proves that a domain finite and unramified over a Dedekind domain is a Dedekind domain. This is needed for #30666.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Artinian/Module.lean

added theorem IsArtinianRing.mem_minimalPrimes

Modified Mathlib/RingTheory/EssentialFiniteness.lean

Modified Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean

added theorem IsLocalization.AtPrime.radical_map_of_mem_minimalPrimes

Modified Mathlib/RingTheory/Localization/Ideal.lean

added theorem IsLocalization.comap_le_comap_iff

Modified Mathlib/RingTheory/TensorProduct/Quotient.lean

added theorem Algebra.TensorProduct.quotIdealMapEquivQuotTensor_mk

Modified Mathlib/RingTheory/Unramified/Basic.lean

Created Mathlib/RingTheory/Unramified/Dedekind.lean

added theorem isDedekindDomain.of_formallyUnramified

added theorem isDedekindDomainDvr.of_formallyUnramified

Modified Mathlib/RingTheory/Unramified/Field.lean

added theorem Algebra.FormallyUnramified.isRadical_map_isMaximal