Commit 2023-03-26 23:21 01f3e275

View on Github →

chore: forward-port leanprover-community/mathlib#18600 (#3005)

Estimated changes

Modified Mathlib/Data/Fintype/Fin.lean

added theorem Fin.Iio_castSucc

added theorem Fin.Iio_last_eq_map

added theorem Fin.map_valEmbedding_univ