equal
deleted
inserted
replaced
660 subsection {* Polynomials form an integral domain *} |
660 subsection {* Polynomials form an integral domain *} |
661 |
661 |
662 lemma coeff_mult_degree_sum: |
662 lemma coeff_mult_degree_sum: |
663 "coeff (p * q) (degree p + degree q) = |
663 "coeff (p * q) (degree p + degree q) = |
664 coeff p (degree p) * coeff q (degree q)" |
664 coeff p (degree p) * coeff q (degree q)" |
665 apply (simp add: coeff_mult) |
665 by (induct p, simp, simp add: coeff_eq_0) |
666 apply (subst setsum_diff1' [where a="degree p"]) |
|
667 apply simp |
|
668 apply simp |
|
669 apply (subst setsum_0' [rule_format]) |
|
670 apply clarsimp |
|
671 apply (subgoal_tac "degree p < a \<or> degree q < degree p + degree q - a") |
|
672 apply (force simp add: coeff_eq_0) |
|
673 apply arith |
|
674 apply simp |
|
675 done |
|
676 |
666 |
677 instance poly :: (idom) idom |
667 instance poly :: (idom) idom |
678 proof |
668 proof |
679 fix p q :: "'a poly" |
669 fix p q :: "'a poly" |
680 assume "p \<noteq> 0" and "q \<noteq> 0" |
670 assume "p \<noteq> 0" and "q \<noteq> 0" |