Theorem Fin.succ_succAbove_predAbove

Modification history

2025-02-03 07:17
Mathlib/Data/Fin/Basic.lean
feat(Order): Fin.succAboveOrderIso (#21303) …
Added Fin.succ_succAbove_predAboveView on Github →