Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.le_of_of_nat_le_of_nat

Modification history

2018-09-13 12:07

data/int/order.lean

feat(data/int/order): delete int.order and prove all commented out lemmas (#348)

Deleted int.le_of_of_nat_le_of_nat View on Github →

2017-08-10 16:36

data/int/order.lean

construct reals as complete, linear ordered field

Added int.le_of_of_nat_le_of_nat View on Github →