equal
deleted
inserted
replaced
1 section \<open>polynomial functions: extremal behaviour and root counts\<close> |
|
2 |
|
3 (* Author: John Harrison and Valentina Bruno |
1 (* Author: John Harrison and Valentina Bruno |
4 Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson |
2 Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson |
5 *) |
3 *) |
6 |
4 |
|
5 section \<open>polynomial functions: extremal behaviour and root counts\<close> |
|
6 |
7 theory PolyRoots |
7 theory PolyRoots |
8 imports Complex_Main |
8 imports Complex_Main |
9 |
|
10 begin |
9 begin |
11 |
10 |
12 subsection\<open>Geometric progressions\<close> |
11 subsection\<open>Geometric progressions\<close> |
13 |
12 |
14 lemma setsum_gp_basic: |
13 lemma setsum_gp_basic: |