Commit 2025-05-15 20:21 aeba9220

View on Github →

feat(BigOperators/Fin): lemmas about summation over intervals (#24358) Add lemmas about sums over Fin.Icc (Fin.castLE h a) (Fin.castLE h b) etc. For Fin.castAdd, Fin.castSucc, and Fin.cast, the set is incomplete, but the missing lemmas will require additions to other files. Also fix the RHS in some recently added lemmas about Finset.map and intervals.

Estimated changes

added theorem Fin.prod_Icc_cast
added theorem Fin.prod_Icc_castAdd
added theorem Fin.prod_Icc_castLE
added theorem Fin.prod_Icc_castSucc
added theorem Fin.prod_Icc_succ
added theorem Fin.prod_Ici_cast
added theorem Fin.prod_Ici_succ
added theorem Fin.prod_Ico_cast
added theorem Fin.prod_Ico_castAdd
added theorem Fin.prod_Ico_castLE
added theorem Fin.prod_Ico_castSucc
added theorem Fin.prod_Ico_succ
added theorem Fin.prod_Iic_cast
added theorem Fin.prod_Iic_castAdd
added theorem Fin.prod_Iic_castLE
added theorem Fin.prod_Iic_castSucc
added theorem Fin.prod_Iio_cast
added theorem Fin.prod_Iio_castAdd
added theorem Fin.prod_Iio_castLE
added theorem Fin.prod_Iio_castSucc
added theorem Fin.prod_Ioc_cast
added theorem Fin.prod_Ioc_castAdd
added theorem Fin.prod_Ioc_castLE
added theorem Fin.prod_Ioc_castSucc
added theorem Fin.prod_Ioc_succ
added theorem Fin.prod_Ioi_cast
modified theorem Fin.prod_Ioi_succ
modified theorem Fin.prod_Ioi_zero
added theorem Fin.prod_Ioo_cast
added theorem Fin.prod_Ioo_castAdd
added theorem Fin.prod_Ioo_castLE
added theorem Fin.prod_Ioo_castSucc
added theorem Fin.prod_Ioo_succ
added theorem Fin.prod_uIcc_cast
added theorem Fin.prod_uIcc_castAdd
added theorem Fin.prod_uIcc_castLE
added theorem Fin.prod_uIcc_castSucc
added theorem Fin.prod_uIcc_succ
modified theorem Fin.map_castAddEmb_Iic
modified theorem Fin.map_castAddEmb_Iio