Commit 2021-10-24 21:16 a30e1900

split(analysis/normed_space/exponential): split file to minimize dependencies (#9932) As suggested by @urkud, this moves all the results depending on derivatives, complex.exp and real.exp to a new file analysis/special_function/exponential. That way the definitions of exp and [complex, real].exp are independent, which means we could eventually redefine the latter in terms of the former without breaking the import tree.