Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-29 02:53 b82ba3c1

View on Github →

feat(data/multiset): multisets are traversable using commutative, applicative functors (#220)

Estimated changes

Modified category/applicative.lean

Modified category/traversable/instances.lean

deleted theorem list.comp_traverse

deleted theorem list.id_traverse

deleted theorem list.naturality

deleted theorem list.traverse_eq_map_id

added theorem traverse_append

Modified category/traversable/lemmas.lean

added theorem traversable.map_traverse'

Modified data/multiset.lean

added theorem multiset.coe_append_eq_add_coe

added theorem multiset.coe_list_cons_eq_cons_coe

added theorem multiset.coe_traverse_cons

added theorem multiset.coe_traverse_cons_swap

added theorem multiset.comp_traverse

added theorem multiset.id_traverse

added theorem multiset.lift_beta

added theorem multiset.map_comp_coe

added theorem multiset.map_traverse

added theorem multiset.naturality

added def multiset.traverse

added theorem multiset.traverse_map