Commit 2025-03-29 16:54 45c1dbdf

View on Github →

chore(Order/Interval): add Fintype.card_Ixx (#23422) Replace *.card_fintypeI* lemmas with generic Fintype.card_I* lemmas.

Estimated changes

added theorem Fintype.card_Icc
added theorem Fintype.card_Ici
added theorem Fintype.card_Ico
added theorem Fintype.card_Iic
added theorem Fintype.card_Iio
added theorem Fintype.card_Ioc
added theorem Fintype.card_Ioi
added theorem Fintype.card_Ioo
added theorem Fintype.card_uIcc
modified theorem Fin.card_fintypeIcc
modified theorem Fin.card_fintypeIci
modified theorem Fin.card_fintypeIco
modified theorem Fin.card_fintypeIic
modified theorem Fin.card_fintypeIio
modified theorem Fin.card_fintypeIoc
modified theorem Fin.card_fintypeIoi
modified theorem Fin.card_fintypeIoo
modified theorem Fin.card_fintype_uIcc
modified theorem Nat.card_fintypeIcc
modified theorem Nat.card_fintypeIco
modified theorem Nat.card_fintypeIic
modified theorem Nat.card_fintypeIio
modified theorem Nat.card_fintypeIoc
modified theorem Nat.card_fintypeIoo