Commit 2023-02-09 22:51 ae5cd168

View on Github →

feat: port Data.Pi.Interval (#2177) This also fixes a mis-port of card_piFinset from #1742, which used Fintype.card instead of the correct Finset.card. After this change the port is just a single name fix.

Estimated changes

modified theorem Fintype.card_pi
added theorem Pi.Icc_eq
added theorem Pi.card_Icc
added theorem Pi.card_Ici
added theorem Pi.card_Ico
added theorem Pi.card_Iic
added theorem Pi.card_Iio
added theorem Pi.card_Ioc
added theorem Pi.card_Ioi
added theorem Pi.card_Ioo