Commit 2023-01-13 14:14 852320cc

View on Github →

feat: port Data.Multiset.Bind (#1537)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Multiset/Bind.lean

added theorem Multiset.add_bind

added theorem Multiset.add_product

added theorem Multiset.add_sigma

added theorem Multiset.attach_bind_coe

added def Multiset.bind

added theorem Multiset.bind_add

added theorem Multiset.bind_assoc

added theorem Multiset.bind_bind

added theorem Multiset.bind_congr

added theorem Multiset.bind_cons

added theorem Multiset.bind_hcongr

added theorem Multiset.bind_map

added theorem Multiset.bind_map_comm

added theorem Multiset.bind_singleton

added theorem Multiset.bind_zero

added theorem Multiset.card_bind

added theorem Multiset.card_join

added theorem Multiset.card_product

added theorem Multiset.card_sigma

added theorem Multiset.coe_bind

added theorem Multiset.coe_join

added theorem Multiset.coe_product

added theorem Multiset.coe_sigma

added theorem Multiset.cons_bind

added theorem Multiset.cons_product

added theorem Multiset.cons_sigma

added theorem Multiset.count_bind

added theorem Multiset.count_sum

added def Multiset.join

added theorem Multiset.join_add

added theorem Multiset.join_cons

added theorem Multiset.join_zero

added theorem Multiset.le_bind

added theorem Multiset.map_bind

added theorem Multiset.mem_bind

added theorem Multiset.mem_join

added theorem Multiset.mem_product

added theorem Multiset.mem_sigma

added theorem Multiset.prod_bind

added def Multiset.product

added theorem Multiset.product_add

added theorem Multiset.product_cons

added theorem Multiset.product_singleton

added theorem Multiset.product_zero

added theorem Multiset.rel_bind

added theorem Multiset.rel_join

added theorem Multiset.sigma_add

added theorem Multiset.sigma_singleton

added theorem Multiset.singleton_bind

added theorem Multiset.singleton_join

added theorem Multiset.zero_bind

added theorem Multiset.zero_product

added theorem Multiset.zero_sigma