Commit 2024-01-08 19:08 77e5628c

feat(Analysis/NormedSpace/TrivSqZeroExt): generalize to topological spaces (#9491) These results are still true even if the exponential does not converge, because in those cases all the terms are zero. The hasSum_fst_expSeries lemma has been dropped because it's a trivial consequence of the new fst_expSeries; the fact that the series are elementwise equal.