Theorem Fin.pred_apply

Modification history

2025-02-06 18:18

Mathlib/Data/Fin/SuccPred.lean

feat(Order): lemmas for `Order.succ` and `Order.pred` in `Fin` (#21437) …

Deleted Fin.pred_apply View on Github →

2023-01-13 10:17

Mathlib/Data/Fin/SuccPred.lean

Feat: Port/data.fin.succ_pred (#1511) …

Added Fin.pred_apply View on Github →