removed redundant DecidableEq instance

leanprover-community · Oct 31, 2024 · 5078654 · 5078654
1 parent d877c16
commit 5078654
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Algebra/MvPolynomial/CommRing.lean b/Mathlib/Algebra/MvPolynomial/CommRing.lean
@@ -99,7 +99,7 @@ section Degrees
 theorem degreeOf_neg (i : σ) (p : MvPolynomial σ R) : degreeOf i (-p) = degreeOf i p := by
   rw [degreeOf, degreeOf, degrees_neg]
 
-theorem degreeOf_sub_le [DecidableEq σ] (i : σ) (p q : MvPolynomial σ R) :
+theorem degreeOf_sub_le (i : σ) (p q : MvPolynomial σ R) :
     degreeOf i (p - q) ≤ max (degreeOf i p) (degreeOf i q) := by
   simpa only [sub_eq_add_neg, degreeOf_neg] using degreeOf_add_le i p (-q)