Analytic order of polynomial evaluation

At zero, the analytic order of polynomial evaluation equals its trailing degree, including infinite order for the zero polynomial. This connects coefficient calculations for polynomial slices to the analytic order used in preparation theorems.

@[simp]

theorem Polynomial.analyticOrderAt_eval_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) : analyticOrderAt (fun (t : 𝕜) => eval t p) 0 = p.trailingDegree

The analytic order at zero of a polynomial function is its trailing degree.