Commit 2024-12-20 15:29 2fbbcf1d

View on Github →

feat: the successor as a function WithBot α → α (#20055) This will be useful to do induction on a family of polynomials by the sum of the successor of their degree. From GrowthInGroups (LeanCamCombi)

Estimated changes

added theorem WithBot.succ_natCast
added theorem WithBot.succ_ofNat
added theorem WithBot.succ_one
added theorem WithBot.succ_zero
added theorem WithBot.orderSucc_bot
added theorem WithBot.orderSucc_coe
deleted theorem WithBot.succ_bot
deleted theorem WithBot.succ_coe
added theorem WithTop.orderPred_coe
added theorem WithTop.orderPred_top
deleted theorem WithTop.pred_coe
deleted theorem WithTop.pred_top
added def WithBot.succ
added theorem WithBot.succ_bot
added theorem WithBot.succ_coe
added theorem WithBot.succ_eq_succ
added theorem WithBot.succ_le_succ
added theorem WithBot.succ_lt_succ
added theorem WithBot.succ_mono
added def WithTop.pred
added theorem WithTop.pred_coe
added theorem WithTop.pred_eq_pred
added theorem WithTop.pred_le_pred
added theorem WithTop.pred_lt_pred
added theorem WithTop.pred_mono
added theorem WithTop.pred_top