Mathlib v3 is deprecated. Go to Mathlib v4

Def real.nnabs

Modification history

2022-09-20 07:09
src/data/real/nnreal.lean
refactor(data/real/basic): make `⊓` and `⊔` computable on reals (#16463) …
Added real.nnabsView on Github →
2021-10-23 20:04
src/data/real/nnreal.lean
chore(data/real): make more instances on real, nnreal, and ennreal computable (#9806) …
Deleted real.nnabsView on Github →
2021-08-24 09:54
src/data/real/nnreal.lean
feat(data/real/nnreal): upgrade `nnabs` to a `monoid_with_zero_hom` (#8844) …
Modified real.nnabsView on Github →
2020-09-11 14:46
src/data/real/nnreal.lean
feat(nnreal): absolute value (#4098)
Added real.nnabsView on Github →