Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.add_val

Modification history

2018-05-24 15:55
analysis/nnreal.lean
feat(analysis/ennreal): add further type class instances for nonnegative reals
Deleted nnreal.add_valView on Github →
2018-05-24 15:55
analysis/nnreal.lean
feat(analysis/nnreal): define the nonnegative reals …
Added nnreal.add_valView on Github →