Commit 2023-03-17 12:30 75957565
View on Github →chore(data/fintype/fin): add Iio lemmas (#18600)
These are the analogue to the existing Ioi lemmas in this file.
Iio_last_eq_map is the dual of Ioi_zero_eq_map, and Iio_cast_succ is the dual of Ioi_succ.
I couldn't find a better home for map_subtype_embedding_univ.
Note that it is deliberately subtype_embedding and not coe_embedding to match the similarly-misnamed fin.map_subtype_embedding_Iio