Commit 2025-06-25 09:23 eefa54b7

View on Github →

chore(Data/Fin/Basic): split off Embedding definitions for Fin (#26260) This PR addresses Tech debt by splitting of embedding-related definitions from Fin.Basic

Estimated changes

deleted def Fin.addNatEmb
deleted def Fin.castAddEmb
deleted theorem Fin.castAddEmb_apply
deleted def Fin.castLEEmb
deleted def Fin.castSuccEmb
deleted theorem Fin.castSuccEmb_apply
deleted theorem Fin.coe_castAddEmb
deleted theorem Fin.coe_castLEEmb
deleted theorem Fin.coe_castSuccEmb
deleted theorem Fin.coe_succAboveEmb
deleted theorem Fin.coe_succEmb
deleted theorem Fin.equiv_iff_eq
deleted def Fin.natAddEmb
deleted def Fin.succAboveEmb
deleted def Fin.succEmb
deleted def Fin.valEmbedding
added def Fin.addNatEmb
added def Fin.castAddEmb
added theorem Fin.castAddEmb_apply
added def Fin.castLEEmb
added def Fin.castSuccEmb
added theorem Fin.castSuccEmb_apply
added theorem Fin.coe_castAddEmb
added theorem Fin.coe_castLEEmb
added theorem Fin.coe_castSuccEmb
added theorem Fin.coe_succAboveEmb
added theorem Fin.coe_succEmb
added theorem Fin.equiv_iff_eq
added def Fin.natAddEmb
added def Fin.succAboveEmb
added def Fin.succEmb
added def Fin.valEmbedding