Theorem Succ.rec

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.rec View on Github →

2023-01-01 19:51

Mathlib/Order/SuccPred/Basic.lean

feat: port Order.SuccPred.Basic (#1233) …

Added Succ.rec View on Github →