chore(ring_theory/adjoin_root): remove some unused decidable_eq (#1530)

leanprover-community · Oct 9, 2019 · 7d792ec · 7d792ec
1 parent a17a9a6
commit 7d792ec
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/ring_theory/adjoin_root.lean b/src/ring_theory/adjoin_root.lean
@@ -16,13 +16,13 @@ variables {α : Type u} {β : Type v} {γ : Type w}
 
 open polynomial ideal
 
-def adjoin_root [comm_ring α] [decidable_eq α] (f : polynomial α) : Type u :=
+def adjoin_root [comm_ring α] (f : polynomial α) : Type u :=
 ideal.quotient (span {f} : ideal (polynomial α))
 
 namespace adjoin_root
 
 section comm_ring
-variables [comm_ring α] [decidable_eq α] (f : polynomial α)
+variables [comm_ring α] (f : polynomial α)
 
 instance : comm_ring (adjoin_root f) := ideal.quotient.comm_ring _