chore: remove IsDedekindDomainDvr

[plp127]

Remove IsDedekindDomainDvr, because is the same as IsDedekindDomain. See Zulip.

---

[github-actions]

PR summary 540ac82250

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ IsDedekindDomain.of_formallyUnramified
+ IsDedekindDomainDvr.dimLEOne
+ isDedekindDomain_iff_isDiscreteValuationRing_atPrime
- IsDedekindDomain.isDedekindDomainDvr
- IsDedekindDomainDvr.isDedekindDomain
- IsDedekindDomainDvr.ring_dimensionLEOne

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 540ac82).

• +2 new declarations
• −11 removed declarations

-IsDedekindDomain.isDedekindDomainDvr
+IsDedekindDomain.of_formallyUnramified
-IsDedekindDomainDvr
-IsDedekindDomainDvr.casesOn
-IsDedekindDomainDvr.isDedekindDomain
-IsDedekindDomainDvr.isIntegrallyClosed
-IsDedekindDomainDvr.is_dvr_at_nonzero_prime
-IsDedekindDomainDvr.mk
-IsDedekindDomainDvr.rec
-IsDedekindDomainDvr.recOn
-IsDedekindDomainDvr.ring_dimensionLEOne
-IsDedekindDomainDvr.toIsNoetherian
+isDedekindDomain_iff_isDiscreteValuationRing_atPrime

---

No changes to strong technical debt.

Decrease in weak tech debt: (relative, absolute) = (1.00, 0.03)

Current number	Change	Type (weak)
32	-1	disabled overlappingInstances linter

Current commit 540ac82250
Reference commit 1f8806b67d

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[kbuzzard]

Suggested change

	- `isDedekindDomain_iff_isDiscreteValuationRing_atPrime` proves the equivalece of
	- `isDedekindDomain_iff_isDiscreteValuationRing_atPrime` proves the equivalence of

[kbuzzard]

So you think we still need this as a def?