Mathlib v3 is deprecated. Go to Mathlib v4

Def pred_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 pred_order.of_core View on Github →