Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-11 14:46 34e0f313

View on Github →

feat(nnreal): absolute value (#4098)

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem real.nnreal.norm_eq

Modified src/data/real/nnreal.lean

added theorem nnreal.abs_eq

added theorem nnreal.coe_nnabs

added def real.nnabs