Commit 2024-09-28 23:34 d453819b

feat: the real exponential is analytic (#17218) Currently, mathlib proves that the complex exponential is analytic as a consequence of its differentiability, quite late in the import hierarchy -- and this is specific to complexes. On the other hand, we also know that the exponential on a general normed algebra is analytic, thanks to its power series expansion. We switch to deduce the former from the latter, earlier in the import hierarchy, and use this occasion to also prove analyticity of the real exponential in the same file.