Commit 2024-09-16 17:23 cedc99c8

View on Github →

feat(Order/SuccPred/TypeTags): SuccOrder (Multiplicative X) and friends (#15940)

Estimated changes

added theorem Order.pred_ofAdd
added theorem Order.pred_ofMul
added theorem Order.pred_toAdd
added theorem Order.pred_toMul
added theorem Order.succ_ofAdd
added theorem Order.succ_ofMul
added theorem Order.succ_toAdd
added theorem Order.succ_toMul