Theorem Fin.val_rev_zero

Modification history

2025-01-22 02:01

Mathlib/Data/Fin/Basic.lean

chore(Data/Fin/Basic): split off `rev` lemmas (#20833) …

Modified Fin.val_rev_zero View on Github →

2024-06-26 15:37

Mathlib/Data/Fin/Basic.lean

feat(Data/Fin/Basic): Expand definition of `BoundedOrder` and `Lattice` for `Fin` (#9814) …

Added Fin.val_rev_zero View on Github →