chore(ring_theory/adjoin_root): remove duplicate namespace (#15775)

leanprover-community · Jul 31, 2022 · b6fa37e · b6fa37e
1 parent 9c473c1
commit b6fa37e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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