equal
deleted
inserted
replaced
1064 then show ?thesis |
1064 then show ?thesis |
1065 unfolding constant_def by auto |
1065 unfolding constant_def by auto |
1066 qed |
1066 qed |
1067 qed |
1067 qed |
1068 |
1068 |
1069 lemma divides_degree: |
|
1070 assumes pq: "p dvd (q:: complex poly)" |
|
1071 shows "degree p \<le> degree q \<or> q = 0" |
|
1072 by (metis dvd_imp_degree_le pq) |
|
1073 |
|
1074 text \<open>Arithmetic operations on multivariate polynomials.\<close> |
1069 text \<open>Arithmetic operations on multivariate polynomials.\<close> |
1075 |
1070 |
1076 lemma mpoly_base_conv: |
1071 lemma mpoly_base_conv: |
1077 fixes x :: "'a::comm_ring_1" |
1072 fixes x :: "'a::comm_ring_1" |
1078 shows "0 = poly 0 x" "c = poly [:c:] x" "x = poly [:0,1:] x" |
1073 shows "0 = poly 0 x" "c = poly [:c:] x" "x = poly [:0,1:] x" |