Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-15 15:46 adfeb249

View on Github →

refactor(algebra/big_operators/order): use to_additive (#7173)

Replace many lemmas about finset.sum with lemmas about finset.prod + @[to_additive];
Avoid s \ t in finset.sum_lt_sum_of_subset.
Use M, N instead of α, β for types with algebraic structures.

Estimated changes

Modified src/algebra/big_operators/order.lean

modified theorem finset.abs_prod

modified theorem finset.abs_sum_le_sum_abs

modified theorem finset.card_le_mul_card_image

modified theorem finset.card_le_mul_card_image_of_maps_to

added theorem finset.exists_le_of_prod_le'

deleted theorem finset.exists_le_of_sum_le

added theorem finset.exists_lt_of_prod_lt'

deleted theorem finset.exists_lt_of_sum_lt

added theorem finset.exists_one_lt_of_prod_one_of_exists_ne_one'

deleted theorem finset.exists_pos_of_sum_zero_of_exists_nonzero

modified theorem finset.le_prod_nonempty_of_submultiplicative

modified theorem finset.le_prod_nonempty_of_submultiplicative_on_pred

modified theorem finset.le_prod_of_submultiplicative

modified theorem finset.le_prod_of_submultiplicative_on_pred

modified theorem finset.mul_card_image_le_card

modified theorem finset.mul_card_image_le_card_of_maps_to

modified theorem finset.prod_add_prod_le'

modified theorem finset.prod_add_prod_le

added theorem finset.prod_eq_one_iff'

added theorem finset.prod_eq_one_iff_of_le_one'

added theorem finset.prod_eq_one_iff_of_one_le'

added theorem finset.prod_fiberwise_le_prod_of_one_le_prod_fiber'

added theorem finset.prod_le_one'

modified theorem finset.prod_le_one

added theorem finset.prod_le_prod''

modified theorem finset.prod_le_prod'

modified theorem finset.prod_le_prod

added theorem finset.prod_le_prod_fiberwise_of_prod_fiber_le_one'

added theorem finset.prod_le_prod_of_ne_one'

added theorem finset.prod_le_prod_of_subset'

added theorem finset.prod_le_prod_of_subset_of_one_le'

added theorem finset.prod_lt_prod'

added theorem finset.prod_lt_prod_of_nonempty'

added theorem finset.prod_lt_prod_of_subset'

added theorem finset.prod_mono_set'

added theorem finset.prod_mono_set_of_one_le'

modified theorem finset.prod_nonneg

modified theorem finset.prod_pos

added theorem finset.single_le_prod'

deleted theorem finset.single_le_sum

added theorem finset.single_lt_prod'

deleted theorem finset.sum_eq_zero_iff

deleted theorem finset.sum_eq_zero_iff_of_nonneg

deleted theorem finset.sum_eq_zero_iff_of_nonpos

deleted theorem finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg

deleted theorem finset.sum_le_sum

deleted theorem finset.sum_le_sum_fiberwise_of_sum_fiber_nonpos

deleted theorem finset.sum_le_sum_of_ne_zero

deleted theorem finset.sum_le_sum_of_subset

deleted theorem finset.sum_le_sum_of_subset_of_nonneg

deleted theorem finset.sum_lt_sum

deleted theorem finset.sum_lt_sum_of_nonempty

deleted theorem finset.sum_lt_sum_of_subset

deleted theorem finset.sum_mono_set

deleted theorem finset.sum_mono_set_of_nonneg

deleted theorem finset.sum_nonneg

deleted theorem finset.sum_nonpos

added theorem fintype.prod_mono'

added theorem fintype.prod_strict_mono'

deleted theorem fintype.sum_mono

deleted theorem fintype.sum_strict_mono

modified theorem with_top.prod_lt_top

modified theorem with_top.sum_eq_top_iff

modified theorem with_top.sum_lt_top

modified theorem with_top.sum_lt_top_iff

Modified src/combinatorics/composition.lean