mathlib

5e58a9dd - chore(docs/undergrad): mention continuity and differentiability of series of functions (#17682)