Commit 2026-09-29 11:07 4802ce0b
View on Github →chore(Calculus/FDeriv/Add): use @[to_fun] for the lemmas about sums (#44202)
Generate the fun_sum versions of the lemmas about the derivative of
∑ i ∈ u, A i with @[to_fun] instead of writing them down, and prove
HasFDerivAtFilter.sum directly from IsLittleO.sum.