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

Estimated changes