Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.val_one

Modification history

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