Higher smoothness of polynomials

We prove that polynomials are C^∞.

theorem Polynomial.contDiff_aeval {R : Type u_1} {𝕜 : Type u_2} [CommSemiring R] [NontriviallyNormedField 𝕜] [Algebra R 𝕜] (f : Polynomial R) (n : WithTop ℕ∞) : ContDiff 𝕜 n fun (x : 𝕜) => (aeval x) f

Polynomials are smooth