Commit 2023-01-13 12:32 069009b9

View on Github →

feat: port Algebra.BigOperators.Multiset.Basic (#1526)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/BigOperators/Multiset/Basic.lean

added theorem Multiset.abs_sum_le_sum_abs

added theorem Multiset.all_one_of_le_one_le_of_prod_eq_one

added theorem Multiset.coe_prod

added theorem Multiset.coe_sumAddMonoidHom

added theorem Multiset.dvd_sum

added theorem Multiset.le_prod_nonempty_of_submultiplicative

added theorem Multiset.le_prod_nonempty_of_submultiplicative_on_pred

added theorem Multiset.le_prod_of_mem

added theorem Multiset.le_prod_of_submultiplicative

added theorem Multiset.le_prod_of_submultiplicative_on_pred

added theorem Multiset.one_le_prod_of_one_le

added theorem Multiset.pow_card_le_prod

added theorem Multiset.pow_count

added def Multiset.prod

added theorem Multiset.prod_add

added theorem Multiset.prod_cons

added theorem Multiset.prod_dvd_prod_of_dvd

added theorem Multiset.prod_dvd_prod_of_le

added theorem Multiset.prod_eq_foldl

added theorem Multiset.prod_eq_foldr

added theorem Multiset.prod_eq_one

added theorem Multiset.prod_eq_pow_single

added theorem Multiset.prod_eq_zero

added theorem Multiset.prod_eq_zero_iff

added theorem Multiset.prod_erase

added theorem Multiset.prod_hom'

added theorem Multiset.prod_hom

added theorem Multiset.prod_hom_rel

added theorem Multiset.prod_hom₂

added theorem Multiset.prod_induction

added theorem Multiset.prod_induction_nonempty

added theorem Multiset.prod_le_pow_card

added theorem Multiset.prod_le_prod_map

added theorem Multiset.prod_le_prod_of_rel_le

added theorem Multiset.prod_map_div

added theorem Multiset.prod_map_eq_pow_single

added theorem Multiset.prod_map_erase

added theorem Multiset.prod_map_inv'

added theorem Multiset.prod_map_inv

added theorem Multiset.prod_map_le_prod

added theorem Multiset.prod_map_le_prod_map

added theorem Multiset.prod_map_mul

added theorem Multiset.prod_map_neg

added theorem Multiset.prod_map_one

added theorem Multiset.prod_map_pow

added theorem Multiset.prod_map_prod_map

added theorem Multiset.prod_map_zpow

added theorem Multiset.prod_ne_zero

added theorem Multiset.prod_nonneg

added theorem Multiset.prod_nsmul

added theorem Multiset.prod_pair

added theorem Multiset.prod_repeat

added theorem Multiset.prod_singleton

added theorem Multiset.prod_toList

added theorem Multiset.prod_zero

added theorem Multiset.single_le_prod

added def Multiset.sumAddMonoidHom

added theorem Multiset.sum_map_mul_left

added theorem Multiset.sum_map_mul_right

added theorem Multiset.sum_map_singleton

added theorem map_multiset_prod

Modified Mathlib/Algebra/Group/Defs.lean