Theorem Order.succ_ofAdd

Modification history

2024-09-16 17:23

Mathlib/Algebra/Order/SuccPred/TypeTags.lean

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

Added Order.succ_ofAdd View on Github →