Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-25 08:42 3bbf8eb8

View on Github →

feat(data/real/nnreal): a few lemmas about subtraction (#1904)

Estimated changes

Modified src/data/real/nnreal.lean

modified theorem nnreal.sub_eq_zero

added theorem nnreal.sub_le_self

added theorem nnreal.sub_self

added theorem nnreal.sub_sub_cancel_of_le

added theorem nnreal.sub_zero