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.
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)