chore(DedekindDomain): drop a DecidableEq assumption (#11532)

leanprover-community · Mar 21, 2024 · b4f1310 · b4f1310
1 parent ebbc0fe
commit b4f1310
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal.lean b/Mathlib/RingTheory/DedekindDomain/Ideal.lean
@@ -712,8 +712,7 @@ theorem Ideal.prime_generator_of_prime {P : Ideal A} (h : Prime P) [P.IsPrincipa
   prime_generator_of_isPrime _ h.ne_zero
 
 open UniqueFactorizationMonoid in
-nonrec theorem Ideal.mem_normalizedFactors_iff [DecidableEq (Ideal A)]
-    {p I : Ideal A} (hI : I ≠ ⊥) :
+nonrec theorem Ideal.mem_normalizedFactors_iff {p I : Ideal A} (hI : I ≠ ⊥) :
     p ∈ normalizedFactors I ↔ p.IsPrime ∧ I ≤ p := by
   rw [← Ideal.dvd_iff_le]
   by_cases hp : p = 0