mathlib

ce86d33b - feat(analysis/calculus/(f)deriv): differentiability of a finite sum of functions (#2657)

feat(analysis/calculus/(f)deriv): differentiability of a finite sum of functions (#2657) We show that, if each `f i` is differentiable, then `λ y, ∑ i in s, f i y` is also differentiable when `s` is a finset, and give the lemmas around this for `fderiv` and `deriv`.