Mathlib v3 is deprecated. Go to Mathlib v4

Def succ_order.of_core

Modification history

2022-04-25 17:22
src/order/succ_pred/basic.lean
feat(data/fin/succ_pred): `fin` is an archimedean succ/pred order (#12792)
Added succ_order.of_coreView on Github →