Mathlib v3 is deprecated. Go to Mathlib v4

Def nnnorm

Modification history

2021-06-23 17:29

src/analysis/normed_space/basic.lean

feat(analysis/normed_space/basic): add has_nnnorm (#7986) …

Deleted nnnorm View on Github →

2020-09-26 12:12

src/analysis/normed_space/basic.lean

feat(ennreal): some lemmas about ennreal (#4262) …

Modified nnnorm View on Github →

2018-08-28 15:08

analysis/normed_space.lean

feat(analysis): add normed spaces

Added nnnorm View on Github →