Commit 2023-06-08 08:49 d950df72

View on Github →

feat: port RingTheory.DedekindDomain.Dvr (#4846)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/DedekindDomain/Dvr.lean

added theorem IsDedekindDomain.isDedekindDomainDvr

added structure IsDedekindDomainDvr

added theorem IsLocalization.AtPrime.discreteValuationRing_of_dedekind_domain

added theorem IsLocalization.AtPrime.isDedekindDomain

added theorem IsLocalization.AtPrime.not_isField

added theorem IsLocalization.isDedekindDomain

added theorem Ring.DimensionLEOne.localization