Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.nnnorm_coe_eq_self

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.nnnorm_coe_eq_selfView on Github →
2020-09-26 12:12
src/analysis/normed_space/basic.lean
feat(ennreal): some lemmas about ennreal (#4262) …
Added real.nnnorm_coe_eq_selfView on Github →