fix(ring_theory/adjoin_root): move adjoin_root out of adjoin_root nam…

…espace

src/ring_theory/adjoin_root.lean

@@ -12,15 +12,16 @@ universes u v w
 
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-namespace adjoin_root
 open polynomial ideal
 
+def adjoin_root [comm_ring α] [decidable_eq α] (f : polynomial α) : Type u :=
+ideal.quotient (span {f} : ideal (polynomial α))
+
+namespace adjoin_root
+
 section comm_ring
 variables [comm_ring α] [decidable_eq α] (f : polynomial α)
 
-def adjoin_root (f : polynomial α) : Type u :=
-ideal.quotient (span {f} : ideal (polynomial α))
-
 instance : comm_ring (adjoin_root f) := ideal.quotient.comm_ring _
 
 noncomputable instance : decidable_eq (adjoin_root f) := classical.dec_eq _