src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 41529 ba60efa2fd08
parent 37887 2ae085b07f2f
child 46240 933f35c4e126
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Jan 12 17:14:27 2011 +0100
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Jan 12 17:19:50 2011 +0100
     1.3 @@ -793,7 +793,7 @@
     1.4    assumes "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
     1.5    and "degree p = n" and "n \<noteq> 0"
     1.6    shows "p dvd (q ^ n)"
     1.7 -using prems
     1.8 +using assms
     1.9  proof(induct n arbitrary: p q rule: nat_less_induct)
    1.10    fix n::nat fix p q :: "complex poly"
    1.11    assume IH: "\<forall>m<n. \<forall>p q.