Theorem Order.succ_toAdd

Modification history

2024-11-22 22:03
Mathlib/Algebra/Order/SuccPred/TypeTags.lean
chore(Algebra/Order/SuccPred/TypeTags): fix defeq abuse with Additive and Multiplicative (#19379) …
Modified Order.succ_toAddView on Github →
2024-09-16 17:23
Mathlib/Algebra/Order/SuccPred/TypeTags.lean
feat(Order/SuccPred/TypeTags): `SuccOrder (Multiplicative X)` and friends (#15940)
Added Order.succ_toAddView on Github →