Commit 2023-07-04 23:32 24d17585

View on Github →

chore: rename Fin.rev to Fin.revPerm (#5715)

Estimated changes

modified theorem Fin.last_sub
deleted def Fin.rev
modified theorem Fin.revOrderIso_symm_apply
added def Fin.revPerm
added theorem Fin.revPerm_bijective
added theorem Fin.revPerm_eq
added theorem Fin.revPerm_inj
added theorem Fin.revPerm_injective
added theorem Fin.revPerm_involutive
added theorem Fin.revPerm_le_revPerm
added theorem Fin.revPerm_lt_revPerm
added theorem Fin.revPerm_revPerm
added theorem Fin.revPerm_surjective
added theorem Fin.revPerm_symm
deleted theorem Fin.rev_bijective
deleted theorem Fin.rev_eq
deleted theorem Fin.rev_inj
deleted theorem Fin.rev_injective
deleted theorem Fin.rev_involutive
deleted theorem Fin.rev_le_rev
deleted theorem Fin.rev_lt_rev
deleted theorem Fin.rev_rev
deleted theorem Fin.rev_surjective
deleted theorem Fin.rev_symm
deleted theorem Fin.val_rev
added theorem Fin.val_revPerm