From 50786542712feacbfffdf2f33194e8656d7b0d31 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Wed, 30 Oct 2024 21:39:01 -0400 Subject: [PATCH] removed redundant `DecidableEq` instance --- Mathlib/Algebra/MvPolynomial/CommRing.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/MvPolynomial/CommRing.lean b/Mathlib/Algebra/MvPolynomial/CommRing.lean index 259c2ca530e11..7d2f5a35c441e 100644 --- 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)