Commit 2025-01-22 02:01 338b4da1

View on Github →

chore(Data/Fin/Basic): split off rev lemmas (#20833) This PR splits out lemmas about the Fin.rev function from Data.Fin.Basic. This addresses an instance of a long file linter trigger.

Estimated changes

deleted theorem Fin.cast_rev
deleted theorem Fin.le_rev_iff
deleted theorem Fin.lt_rev_iff
deleted theorem Fin.predAbove_rev_left
deleted theorem Fin.predAbove_rev_right
deleted def Fin.revPerm
deleted theorem Fin.revPerm_symm
deleted theorem Fin.rev_bijective
deleted theorem Fin.rev_castPred
deleted theorem Fin.rev_eq_iff
deleted theorem Fin.rev_injective
deleted theorem Fin.rev_involutive
deleted theorem Fin.rev_le_iff
deleted theorem Fin.rev_lt_iff
deleted theorem Fin.rev_ne_iff
deleted theorem Fin.rev_pred
deleted theorem Fin.rev_predAbove
deleted theorem Fin.rev_succAbove
deleted theorem Fin.rev_surjective
deleted theorem Fin.succAbove_rev_left
deleted theorem Fin.succAbove_rev_right
deleted theorem Fin.val_rev_zero
added theorem Fin.cast_rev
added theorem Fin.le_rev_iff
added theorem Fin.lt_rev_iff
added theorem Fin.predAbove_rev_left
added def Fin.revPerm
added theorem Fin.revPerm_symm
added theorem Fin.rev_bijective
added theorem Fin.rev_castPred
added theorem Fin.rev_eq_iff
added theorem Fin.rev_injective
added theorem Fin.rev_involutive
added theorem Fin.rev_le_iff
added theorem Fin.rev_lt_iff
added theorem Fin.rev_ne_iff
added theorem Fin.rev_pred
added theorem Fin.rev_predAbove
added theorem Fin.rev_succAbove
added theorem Fin.rev_surjective
added theorem Fin.succAbove_rev_left
added theorem Fin.val_rev_zero