equal
deleted
inserted
replaced
770 lemma poly_roots_finite_set: "poly p \<noteq> poly [] ==> finite {x::'a::{idom,ring_char_0}. poly p x = 0}" |
770 lemma poly_roots_finite_set: "poly p \<noteq> poly [] ==> finite {x::'a::{idom,ring_char_0}. poly p x = 0}" |
771 unfolding poly_roots_finite . |
771 unfolding poly_roots_finite . |
772 |
772 |
773 text{*bound for polynomial.*} |
773 text{*bound for polynomial.*} |
774 |
774 |
775 lemma poly_mono: "abs(x) \<le> k ==> abs(poly p (x::'a::{ordered_idom})) \<le> poly (map abs p) k" |
775 lemma poly_mono: "abs(x) \<le> k ==> abs(poly p (x::'a::{linordered_idom})) \<le> poly (map abs p) k" |
776 apply (induct "p", auto) |
776 apply (induct "p", auto) |
777 apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans) |
777 apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans) |
778 apply (rule abs_triangle_ineq) |
778 apply (rule abs_triangle_ineq) |
779 apply (auto intro!: mult_mono simp add: abs_mult) |
779 apply (auto intro!: mult_mono simp add: abs_mult) |
780 done |
780 done |