Theorem succ_min

Modification history

2024-09-08 12:47

Mathlib/Order/SuccPred/Archimedean.lean

chore(Order/SuccPred/Basic): Move succ/pred being archimedean to a different file (#16559) …

Modified succ_min View on Github →

2024-03-08 21:06

Mathlib/Order/SuccPred/Basic.lean

feat(SuccPred): {succ,pred}_{min,max} (#9367)

Added succ_min View on Github →