Commit 2021-10-16 18:01 155f8e66

View on Github →

feat(data/int/succ_pred): ℤ is succ- and pred- archimedean (#9731) This provides the instances succ_order ℤ, pred_order ℤ, is_succ_archimedean ℤ, is_pred_archimedean ℤ.

Estimated changes

Created src/data/int/succ_pred.lean

added theorem int.pred_iterate

added theorem int.succ_iterate

Modified src/order/succ_pred.lean

added def pred_order.of_le_pred_iff

added def pred_order.of_le_pred_iff_of_pred_le_pred

deleted def pred_order.pred_order_of_le_pred_iff

deleted def pred_order.pred_order_of_le_pred_iff_of_pred_le_pred

added def succ_order.of_succ_le_iff

added def succ_order.of_succ_le_iff_of_le_lt_succ

deleted def succ_order.succ_order_of_succ_le_iff

deleted def succ_order.succ_order_of_succ_le_iff_of_le_lt_succ