From b6fa37edf53f0713db3fb2b727cdec05eef97637 Mon Sep 17 00:00:00 2001
From: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Date: Sun, 31 Jul 2022 15:17:21 +0000
Subject: [PATCH] chore(ring_theory/adjoin_root): remove duplicate namespace
 (#15775)

---
 src/ring_theory/adjoin_root.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ring_theory/adjoin_root.lean b/src/ring_theory/adjoin_root.lean
index ef8f030aa82c5..69f6fbe3aafb0 100644
--- a/src/ring_theory/adjoin_root.lean
+++ b/src/ring_theory/adjoin_root.lean
@@ -107,7 +107,7 @@ def root : adjoin_root f := mk f X
 
 variables {f}
 
-instance adjoin_root.has_coe_t : has_coe_t R (adjoin_root f) := ⟨of f⟩
+instance has_coe_t : has_coe_t R (adjoin_root f) := ⟨of f⟩
 
 @[simp] lemma mk_eq_mk {g h : R[X]} : mk f g = mk f h ↔ f ∣ g - h :=
 ideal.quotient.eq.trans ideal.mem_span_singleton