Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.nnreal.norm_eq

Modification history

2021-02-10 00:03
src/analysis/normed_space/basic.lean
feat(measure_theory/lp_space): add more API on Lp spaces (#6042) …
Deleted real.nnreal.norm_eqView on Github →
2020-09-11 14:46
src/analysis/normed_space/basic.lean
feat(nnreal): absolute value (#4098)
Added real.nnreal.norm_eqView on Github →