mathlib

563bbc0c - feat(analysis/calculus): smoothness of series of functions (#17110)

feat(analysis/calculus): smoothness of series of functions (#17110) We show that infinite series of functions are continuous/differentiable/smooth under suitable summability assumptions.