src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 62128 3201ddb00097
parent 61945 1135b8de26c3
child 63060 293ede07b775
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jan 11 15:20:17 2016 +0100
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jan 11 16:38:39 2016 +0100
     1.3 @@ -1066,11 +1066,6 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -lemma divides_degree:
     1.8 -  assumes pq: "p dvd (q:: complex poly)"
     1.9 -  shows "degree p \<le> degree q \<or> q = 0"
    1.10 -  by (metis dvd_imp_degree_le pq)
    1.11 -
    1.12  text \<open>Arithmetic operations on multivariate polynomials.\<close>
    1.13  
    1.14  lemma mpoly_base_conv: