Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-05 08:42 c782e282

View on Github →

chore(analysis/normed_space/units): add protected, minor review (#6544)

Estimated changes

deleted theorem units.is_open
deleted theorem units.nhds