Commit 2024-01-10 10:28 2d16ed00

feat(Mathlib/Analysis/Analytic): continuously polynomial functions (#9269) This defines "continuously polynomial" (shortened to "cpolynomial") functions as a special cases of analytic functions: they are the functions that admit a development as a finite formal multilinear series. Then we prove their basic properties. The point of doing is this is that finite series are always summable, so we can remove the completeness assumptions in some results about analytic functions (differentiability for example). Examples of continuously polynomial functions include continuous multilinear maps, and functions defined by polynomials.