Commit 2024-02-01 07:10 09303adf

View on Github →

feat(Data/Fin/Basic): Add missing succAbove and predAbove lemmas and refactor existing ones. (#10042) Adds lemma that shows that succAbove and castSucc commute and similar for predAbove. Perform necessary updates and refactors to get there.

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.castPred_succAbove_castPred

added theorem Fin.castSucc_predAbove_castSucc

added theorem Fin.castSucc_succAbove_castSucc

added theorem Fin.ne_succAbove

added theorem Fin.rev_predAbove

added theorem Fin.succAbove_eq_last_iff

modified theorem Fin.succAbove_lt_ge

added theorem Fin.succAbove_ne_last

added theorem Fin.succAbove_ne_last_last

modified theorem Fin.succAbove_right_inj

added theorem Fin.succAbove_zero_apply