mathlib3
a30e1900 - split(analysis/normed_space/exponential): split file to minimize dependencies (#9932)

Commit
4 years ago
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.
Author
Parents
Loading