Commit 2023-03-21 18:09 4f604a1b

View on Github →

chore: fix bad names of ported lemmas (#3004) These lemmas are about valEmbedding, not a non-existant subtype_embedding. The mathlib3 name was wrong too, but there's no need to backport this thanks to #align. At any rate, the correct mathlib3 name would have been coe_embedding.

Estimated changes

Modified Mathlib/Data/Fin/Interval.lean

deleted theorem Fin.map_subtype_embedding_Icc

deleted theorem Fin.map_subtype_embedding_Ici

deleted theorem Fin.map_subtype_embedding_Ico

deleted theorem Fin.map_subtype_embedding_Iic

deleted theorem Fin.map_subtype_embedding_Iio

deleted theorem Fin.map_subtype_embedding_Ioc

deleted theorem Fin.map_subtype_embedding_Ioi

deleted theorem Fin.map_subtype_embedding_Ioo

added theorem Fin.map_valEmbedding_Icc

added theorem Fin.map_valEmbedding_Ici

added theorem Fin.map_valEmbedding_Ico

added theorem Fin.map_valEmbedding_Iic

added theorem Fin.map_valEmbedding_Iio

added theorem Fin.map_valEmbedding_Ioc

added theorem Fin.map_valEmbedding_Ioi

added theorem Fin.map_valEmbedding_Ioo