Commit 2024-05-05 12:47 f98db542

feat: add HasSum f a → HasProd (exp ∘ f) (exp a) (#12635) This adds lemmas saying that HasSum f a implies HasProd (exp ∘ f) (exp a) for exp = rexp, cexp, NormedSpace.exp. While the rexp and cexp versions could be deduced from the NormedSpace.exp one, we give a direct proof (and so avoid needing to import stuff about NormedSpace.exp for these results; the proofs are also a bit faster that way). Based on the discussion below, this also renames Filter.Tendsto.exp to Filter.Tendsto.rexp for the version specific to the real exponential function, so that Filter.Tendsto.exp can be used for the corresponding statement involving NormedSpace.exp. See here on Zulip.