Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-18 00:18 9607bbf8

View on Github →

feat(algebra/big_operators): sum_Ico_succ_top and others (#1692)

feat(Ico): sum_Ico_succ_top and others
get rid of succ_bot and rename eq_cons

Estimated changes

Modified src/algebra/big_operators.lean

added theorem finset.prod_Ico_succ_top

added theorem finset.prod_eq_prod_Ico_succ_bot

added theorem finset.sum_Ico_succ_top

added theorem finset.sum_eq_sum_Ico_succ_bot

Modified src/data/finset.lean

deleted theorem finset.Ico.eq_cons

added theorem finset.Ico.insert_succ_bot