Commit 2023-12-30 02:31 b060d4a1

View on Github →

chore(Data/Fintype/Fin): golf a proof (#9336) We already have it for Set.range.

Estimated changes

Modified Mathlib/Data/Fintype/Fin.lean

modified theorem Fin.Iio_last_eq_map

modified theorem Fin.Ioi_zero_eq_map