Commit 2025-07-15 11:35 f96ef6f7

View on Github →

feat: add Mathlib.RingTheory.DedekindDomain.Instances (#26070) We add a new file Mathlib.RingTheory.DedekindDomain.Instances containing various instances that are useful to work with the localization a prime of an extension of Dedekind domains. As a practical example we golf a tedious proof in Mathlib.RingTheory.Ideal/Norm.RelNorm.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Created Mathlib/RingTheory/DedekindDomain/Instances.lean

added theorem FractionRing.isSeparable_of_isLocalization

added theorem algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

Modified Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

Modified Mathlib/RingTheory/Localization/AtPrime.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

added theorem IsLocalization.algEquiv_comp_algebraMap

added theorem IsLocalization.algEquiv_comp_algebraMap_apply

Modified Mathlib/RingTheory/Localization/Ideal.lean

Modified Mathlib/RingTheory/Localization/LocalizationLocalization.lean

Modified Mathlib/RingTheory/RingHom/Finite.lean

added theorem Module.Finite.of_isLocalization

deleted theorem Module.Finite_of_isLocalization

Modified Mathlib/RingTheory/Trace/Quotient.lean