| changeset 69683 | 8b3458ca0762 |
| parent 69517 | dc20f278e8f3 |
| child 69730 | 0c3dcb3a17f6 |
--- a/src/HOL/Analysis/Poly_Roots.thy Thu Jan 17 16:37:06 2019 -0500 +++ b/src/HOL/Analysis/Poly_Roots.thy Thu Jan 17 16:38:00 2019 -0500 @@ -8,7 +8,7 @@ imports Complex_Main begin -subsection%important\<open>Basics about polynomial functions: extremal behaviour and root counts\<close> +subsection\<open>Basics about polynomial functions: extremal behaviour and root counts\<close> lemma%important sub_polyfun: fixes x :: "'a::{comm_ring,monoid_mult}"