Def Fin2.last

Modification history

2025-07-11 21:09
Mathlib/Data/Fin/Fin2.lean
chore: `n+1` to `n + 1` (#26937)
Modified Fin2.lastView on Github →
2024-06-06 10:40
Mathlib/Data/Fin/Fin2.lean
feat: define `Fin2.rev` analogously to `Fin.rev` (#10818) …
Added Fin2.lastView on Github →