Mathlib v3 is deprecated. Go to Mathlib v4

Theorem units.nhds

Modification history

2021-03-05 08:42
src/analysis/normed_space/units.lean
chore(analysis/normed_space/units): add `protected`, minor review (#6544)
Deleted units.nhdsView on Github →
2020-08-02 03:20
src/analysis/normed_space/units.lean
feat(analysis/calculus/times_cont_diff): inversion is smooth (#3639) …
Added units.nhdsView on Github →