Commit 2023-01-20 09:47 cc097f54

View on Github →

feat: port Algebra.BigOperators.Order (#1673)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/BigOperators/Order.lean

added theorem AbsoluteValue.map_prod

added theorem AbsoluteValue.sum_le

added theorem Finset.abs_prod

added theorem Finset.abs_sum_le_sum_abs

added theorem Finset.abs_sum_of_nonneg'

added theorem Finset.abs_sum_of_nonneg

added theorem Finset.card_bunionᵢ_le_card_mul

added theorem Finset.card_le_card_bunionᵢ

added theorem Finset.card_le_card_bunionᵢ_add_card_fiber

added theorem Finset.card_le_card_bunionᵢ_add_one

added theorem Finset.card_le_mul_card_image

added theorem Finset.card_le_mul_card_image_of_maps_to

added theorem Finset.exists_le_of_prod_le'

added theorem Finset.exists_lt_of_prod_lt'

added theorem Finset.exists_one_lt_of_prod_one_of_exists_ne_one'

added theorem Finset.le_prod_nonempty_of_submultiplicative

added theorem Finset.le_prod_nonempty_of_submultiplicative_on_pred

added theorem Finset.le_prod_of_submultiplicative

added theorem Finset.le_prod_of_submultiplicative_on_pred

added theorem Finset.le_sum_card

added theorem Finset.le_sum_card_inter

added theorem Finset.mul_card_image_le_card

added theorem Finset.mul_card_image_le_card_of_maps_to

added theorem Finset.one_le_prod''

added theorem Finset.one_le_prod'

added theorem Finset.one_lt_prod'

added theorem Finset.one_lt_prod

added theorem Finset.pow_card_le_prod

added theorem Finset.prod_add_prod_le'

added 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_eq_prod_iff_of_le

added theorem Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber'

added theorem Finset.prod_le_one'

added theorem Finset.prod_le_one

added theorem Finset.prod_le_pow_card

added theorem Finset.prod_le_prod''

added theorem Finset.prod_le_prod'

added 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_le_univ_prod_of_one_le'

added theorem Finset.prod_lt_one'

added theorem Finset.prod_lt_one

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'

added theorem Finset.prod_nonneg

added theorem Finset.prod_pos

added theorem Finset.single_le_prod'

added theorem Finset.single_lt_prod'

added theorem Finset.sum_card

added theorem Finset.sum_card_inter

added theorem Finset.sum_card_inter_le

added theorem Finset.sum_card_le

added theorem Fintype.prod_mono'

added theorem Fintype.prod_strict_mono'

added theorem IsAbsoluteValue.abv_sum

added theorem IsAbsoluteValue.map_prod

added theorem WithTop.prod_lt_top

added theorem WithTop.sum_eq_top_iff

added theorem WithTop.sum_lt_top

added theorem WithTop.sum_lt_top_iff