Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-24 15:55 02f8f481

View on Github →

feat(analysis/nnreal): define the nonnegative reals NB: This file has a lot in common with ennreal.lean, the extended nonnegative reals.

Estimated changes

added theorem nnreal.add_val
added theorem nnreal.le_zero_iff_eq
added theorem nnreal.mul_val
added theorem nnreal.val_one
added theorem nnreal.val_zero