Theorem toZ_iterate_pred_ge

Modification history

2023-06-29 23:57

Mathlib/Order/SuccPred/LinearLocallyFinite.lean

fix precedence of `Nat.iterate` (#5589)

Modified toZ_iterate_pred_ge View on Github →

2023-02-03 06:59

Mathlib/Order/SuccPred/LinearLocallyFinite.lean

feat: port Order.SuccPred.LinearLocallyFinite (#2033)

Added toZ_iterate_pred_ge View on Github →