Commit 2024-11-18 12:21 5fbd4a73

View on Github →

chore: move Fin material earlier (#19186) This will in particular be used in #19086 to prove Finite Bool and Finite Prop much earlier.

Estimated changes

added def Fin.consEquiv
added def Fin.snocEquiv
added def piFinTwoEquiv
added def finOneEquiv
added def finTwoEquiv
added def finZeroEquiv'
added def finZeroEquiv
deleted def Fin.consEquiv
deleted def Fin.insertNthEquiv
deleted theorem Fin.insertNthEquiv_last
deleted theorem Fin.insertNthEquiv_zero
deleted def Fin.snocEquiv
deleted def finOneEquiv
deleted def finTwoEquiv
deleted def finZeroEquiv'
deleted def finZeroEquiv
deleted def piFinTwoEquiv