Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-10 15:29 2cd640a5

View on Github →

feat(data/multiset): add sections

Estimated changes

Modified data/list/basic.lean

added theorem list.bind_map

Modified data/multiset.lean

added theorem multiset.bind_add

added theorem multiset.bind_assoc

modified theorem multiset.bind_bind

added theorem multiset.bind_cons

added theorem multiset.bind_map

added theorem multiset.bind_map_comm

added theorem multiset.bind_zero

added theorem multiset.card_sections

added theorem multiset.coe_sections

modified theorem multiset.map_bind

added theorem multiset.map_id'

added theorem multiset.mem_sections

added theorem multiset.prod_map_one

added theorem multiset.prod_map_sum

added theorem multiset.rel_bind

added def multiset.sections

added theorem multiset.sections_add

added theorem multiset.sections_cons

added theorem multiset.sections_zero

added theorem multiset.sum_map_mul_left

added theorem multiset.sum_map_mul_right

added theorem multiset.sum_map_zero