Commit 2023-10-25 13:20 34d930ad

feat(Analysis/Analytic): A few lemmas that simple things are analytic (#7677) We record various simple lemmas that things are analyticAt or analyticOn. There's no hard work here, just corollaries of other results:

1. id, fst, snd
2. Power series terms, in the origin (we already know they have power series, this is just the .analyticAt_changeOrigin corollary
3. Finite sums
4. Pairs of analytic functions: x ↦ (f x, g x) We also add a few lemmas for dealing with curried analytic functions. Starting with AnalyticOn 𝕜 (uncurry h) s,
5. AnalyticOn.curry_comp composes it with two input analytic functions
6. AnalyticOn.along_fst/snd show analyticity along each coordinate