Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-07 13:46 eef3a4d5

View on Github →

feat(data/multiset): add map_hcongr, bind_hcongr, bind_bind, attach_zero, and attach_cons

Estimated changes

Modified data/multiset.lean

added theorem multiset.attach_cons

added theorem multiset.attach_zero

added theorem multiset.bind_bind

added theorem multiset.bind_congr

added theorem multiset.bind_hcongr

added theorem multiset.card_singleton

added theorem multiset.count_bind

added theorem multiset.map_bind

added theorem multiset.map_hcongr

added theorem multiset.mem_cons_of_mem

added theorem multiset.prod_map_mul

added theorem multiset.prod_map_prod_map