Theorem Fin.succAbove_lt_gt
Modification history
2024-01-17 15:11
Mathlib/Data/Fin/Basic.lean
fix(Data/Fin/Basic): Change definition of `predAbove` to use `castPred` (#9791) …
Deleted Fin.succAbove_lt_gtView on Github →2023-07-13 01:24
Mathlib/Data/Fin/Basic.lean
chore: bump to nightly-2023-07-01 (#5409) …
Modified Fin.succAbove_lt_gtView on Github →