Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-19 22:11 f5446325

View on Github →

feat(algebra/big_operators): products and sums over finset.Ico (#1567)

Estimated changes

Modified src/algebra/big_operators.lean

added theorem finset.prod_Ico_add

added theorem finset.prod_Ico_consecutive

added theorem finset.prod_Ico_eq_div

added theorem finset.prod_Ico_eq_prod_range

added theorem finset.prod_range_mul_prod_Ico

added theorem finset.sum_Ico_add

added theorem finset.sum_Ico_eq_sub

Modified src/data/finset.lean

added theorem finset.Ico.disjoint_consecutive

modified theorem finset.Ico.inter_consecutive

modified theorem finset.Ico.self_eq_empty

modified theorem finset.Ico.succ_singleton