equal
deleted
inserted
replaced
6 |
6 |
7 theory Poly_Roots |
7 theory Poly_Roots |
8 imports Complex_Main |
8 imports Complex_Main |
9 begin |
9 begin |
10 |
10 |
11 subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close> |
11 subsection\<open>Basics about polynomial functions: extremal behaviour and root counts\<close> |
12 |
12 |
13 lemma sub_polyfun: |
13 lemma sub_polyfun: |
14 fixes x :: "'a::{comm_ring,monoid_mult}" |
14 fixes x :: "'a::{comm_ring,monoid_mult}" |
15 shows "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) = |
15 shows "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) = |
16 (x - y) * (\<Sum>j<n. \<Sum>k= Suc j..n. a k * y^(k - Suc j) * x^j)" |
16 (x - y) * (\<Sum>j<n. \<Sum>k= Suc j..n. a k * y^(k - Suc j) * x^j)" |