src/HOL/Library/Fundamental_Theorem_Algebra.thy

   unfolding constant_def psize_def
   apply (induct p, auto)
   done
 
 lemma poly_replicate_append:
-  "poly (monom 1 n * p) (x::'a::{recpower, comm_ring_1}) = x^n * poly p x"
+  "poly (monom 1 n * p) (x::'a::{comm_ring_1}) = x^n * poly p x"
   by (simp add: poly_monom)
 
 text {* Decomposition of polynomial, skipping zero coefficients
   after the first.  *}
 
 lemma poly_decompose_lemma:
- assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{recpower,idom}))"
+ assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{idom}))"
   shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and>
                  (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
 unfolding psize_def
 using nz
 proof(induct p)

   ultimately show ?case by blast
 qed
 
 lemma poly_decompose:
   assumes nc: "~constant(poly p)"
-  shows "\<exists>k a q. a\<noteq>(0::'a::{recpower,idom}) \<and> k\<noteq>0 \<and>
+  shows "\<exists>k a q. a\<noteq>(0::'a::{idom}) \<and> k\<noteq>0 \<and>
                psize q + k + 1 = psize p \<and>
               (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
 using nc
 proof(induct p)
   case 0 thus ?case by (simp add: constant_def)