Commit 2024-06-26 15:37 fed9531b

View on Github →

feat(Data/Fin/Basic): Expand definition of BoundedOrder and Lattice for Fin (#9814) Redefine the BoundedOrder and Lattice on Fin (n + 1) so that they are defined for Fin n.

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

modified theorem Fin.one_lt_last

modified theorem Fin.rev_involutive

added theorem Fin.val_rev_zero

Modified Mathlib/Order/Fin.lean

added theorem Fin.rev_bot

added theorem Fin.rev_last_eq_bot

added theorem Fin.rev_top

added theorem Fin.rev_zero_eq_top