Commit 2026-08-10 10:19 5d2a6a32

View on Github →

chore: remove IsDedekindDomainDvr (#42367) Remove IsDedekindDomainDvr, because is the same as IsDedekindDomain. See Zulip.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/ExistsRamified.lean

Modified Mathlib/RingTheory/DedekindDomain/Basic.lean

Modified Mathlib/RingTheory/DedekindDomain/Dvr.lean

modified theorem IsLocalization.AtPrime.not_isField

Modified Mathlib/RingTheory/Trace/Quotient.lean

Modified Mathlib/RingTheory/Unramified/Dedekind.lean

added theorem IsDedekindDomain.of_formallyUnramified

deleted theorem isDedekindDomain.of_formallyUnramified

deleted theorem isDedekindDomainDvr.of_formallyUnramified