Commit 2026-01-19 07:36 fadadaad

chore(Analysis/Distribution): split off derivatives from SchwartzSpace and create new folder (#34027) Since Analysis/Distribution/SchwartzSpace.lean is over 1500 lines, we have to move some of its contents into a new file. The derivatives are a natural choice, because it is quite a few lines of code, will see further expansion (with the Laplacian) and a number of imports are just needed for them. We perform this split by moving the current file to Analysis/Distribution/SchwartzSpace/Basic.lean and creating a new file Analysis/Distribution/SchwartzSpace.Deriv.lean. Moreover, we move the previous Analysis/Distribution/FourierSchwartz.lean to Analysis/Distribution/SchwartzSpace/Fourier.lean