Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.sub_one_le_iff

Modification history

2018-10-07 09:09

data/int/basic.lean

fix(data/int.basic): rename sub_one_le_iff (#394)

Deleted int.sub_one_le_iff View on Github →

2018-01-16 05:29

data/int/basic.lean

feat(data/real): completeness of the (new) real numbers

Added int.sub_one_le_iff View on Github →