Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-06-28 19:09
08b07a64
View on Github →
feat(order/succ_pred/basic): tag more lemmas with simp (
#14998
)
Estimated changes
Modified
src/order/succ_pred/basic.lean
modified
theorem
order.Icc_pred_right
modified
theorem
order.Icc_succ_left
modified
theorem
order.Ico_succ_left
modified
theorem
order.Ico_succ_right
modified
theorem
order.Ioc_pred_left
modified
theorem
order.Ioc_pred_right
modified
theorem
order.Ioo_pred_left
modified
theorem
order.Ioo_succ_right
modified
theorem
order.le_pred_iff
modified
theorem
order.lt_succ_iff
modified
theorem
order.pred_le_pred_iff
modified
theorem
order.pred_lt_iff
modified
theorem
order.pred_lt_pred_iff
modified
theorem
order.succ_le_iff
modified
theorem
order.succ_le_succ_iff
modified
theorem
order.succ_lt_succ_iff