From c54e60f878b512250bfe1742d5d896dd5305ca8e Mon Sep 17 00:00:00 2001
From: Yongle Hu <140475041+mbkybky@users.noreply.github.com>
Date: Sat, 11 Jul 2026 09:55:42 +0800
Subject: [PATCH 1/2] Update Dvr.lean

---
 Mathlib/RingTheory/DedekindDomain/Dvr.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Dvr.lean b/Mathlib/RingTheory/DedekindDomain/Dvr.lean
index 148e5ee14fe445..536014532a3bfc 100644
--- a/Mathlib/RingTheory/DedekindDomain/Dvr.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Dvr.lean
@@ -56,7 +56,7 @@ localization at every nonzero prime is a discrete valuation ring.
 
 This is equivalent to `IsDedekindDomain`.
 -/
-class IsDedekindDomainDvr : Prop extends IsNoetherian A A where
+class IsDedekindDomainDvr : Prop extends IsNoetherianRing A where
   is_dvr_at_nonzero_prime : ∀ P ≠ (⊥ : Ideal A), ∀ _ : P.IsPrime,
     IsDiscreteValuationRing (Localization.AtPrime P)
 

From 78aef9280c9374076cfb3d6fa00cdd1f20564597 Mon Sep 17 00:00:00 2001
From: Yongle Hu <140475041+mbkybky@users.noreply.github.com>
Date: Sat, 11 Jul 2026 10:04:50 +0800
Subject: [PATCH 2/2] Update Basic.lean

---
 Mathlib/RingTheory/DedekindDomain/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Basic.lean b/Mathlib/RingTheory/DedekindDomain/Basic.lean
index 836e591313a5c6..9fad076f377f6f 100644
--- a/Mathlib/RingTheory/DedekindDomain/Basic.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Basic.lean
@@ -116,7 +116,7 @@ The integral closure condition is independent of the choice of field of fraction
 use `isDedekindRing_iff` to prove `IsDedekindRing` for a given `fraction_map`.
 -/
 class IsDedekindRing : Prop
-  extends IsNoetherian A A, DimensionLEOne A, IsIntegralClosure A A (FractionRing A)
+  extends IsNoetherianRing A, DimensionLEOne A, IsIntegralClosure A A (FractionRing A)
 
 /-- An integral domain is a Dedekind domain if and only if it is
 Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field.