Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-24 15:55 9303bc02

View on Github →

feat(analysis/ennreal): add further type class instances for nonnegative reals

Estimated changes

Modified algebra/ordered_group.lean

added theorem le_zero_iff_eq

Modified analysis/nnreal.lean

deleted theorem nnreal.add_val

deleted theorem nnreal.le_zero_iff_eq

deleted theorem nnreal.mul_val

deleted theorem nnreal.val_one

deleted theorem nnreal.val_zero

Modified set_theory/cofinality.lean