Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-02 15:22 a99f9b55

View on Github →

refactor(algebra/big_operators): introduce notation for finset.prod and finset.sum (#2582) I have not gone through all of mathlib to use this notation everywhere. I think we can maybe transition naturally.

Estimated changes

modified theorem finset.card_eq_sum_ones
modified theorem finset.exists_le_of_sum_le
modified theorem finset.mul_sum
deleted theorem finset.prod_Ico_eq_div
modified theorem finset.prod_Ico_id_eq_fact
modified theorem finset.prod_attach
modified theorem finset.prod_const
modified theorem finset.prod_const_one
modified theorem finset.prod_empty
modified theorem finset.prod_eq_fold
modified theorem finset.prod_eq_one
modified theorem finset.prod_eq_zero
modified theorem finset.prod_eq_zero_iff
modified theorem finset.prod_filter_ne_one
modified theorem finset.prod_insert
modified theorem finset.prod_inv_distrib
modified theorem finset.prod_mul_distrib
modified theorem finset.prod_pos
modified theorem finset.prod_sdiff
modified theorem finset.prod_singleton
modified theorem finset.prod_subset
modified theorem finset.prod_union
modified theorem finset.single_le_sum
modified theorem finset.sum_le_sum
modified theorem finset.sum_le_sum_of_subset
modified theorem finset.sum_mul
modified theorem finset.sum_nonneg
modified theorem finset.sum_nonpos
modified theorem finset.sum_range_id
added theorem finset.sum_range_succ
modified theorem finset.sum_sub_distrib