Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.of_nat_le_of_nat_of_le

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.of_nat_le_of_nat_of_le View on Github →

2017-08-10 16:36

data/int/order.lean

construct reals as complete, linear ordered field

Added int.of_nat_le_of_nat_of_le View on Github →