Commit 2019-04-10 17:49 f5d43a95
View on Github →feat(analysis/normed_space/deriv): show that the differential is unique (2) (#916)
- Remove wrong simp attribute
- fix typo
- characterize convergence at_top in normed spaces
- copy some changes from #829
- small elements in normed fields go to zero
- derivatives are unique
- remove unnecessary lemma
- update according to review
- remove another empty line