mathlib3
ade99c8c - feat(analysis/normed_space/deriv): more material on derivatives (#966)

Commit
6 years ago
feat(analysis/normed_space/deriv): more material on derivatives (#966) * feat(analysis/normed_space/deriv): more material on derivatives * feat(analysis/normed_space/deriv): minor improvements * feat(analysis/normed_space/deriv) rename fderiv_at_within to fderiv_within_at * feat(analysis/normed_space/deriv): more systematic renaming * feat(analysis/normed_space/deriv): fix style * modify travis.yml as advised by Simon Hudon * fix travis.yml, second try * feat(analysis/normed_space/deriv): add two missing lemmas
Author
Committer
Parents
Loading