mathlib3

feat(analysis/normed_space/deriv): more material on derivatives

#966

Merged