Commit 2023-01-31 17:29 583f6cfa

View on Github →

feat: Port data.multiset.functor (#1790)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Multiset/Functor.lean

added theorem Multiset.bind_def

added theorem Multiset.comp_traverse

added theorem Multiset.fmap_def

added theorem Multiset.id_traverse

added theorem Multiset.lift_coe

added theorem Multiset.map_comp_coe

added theorem Multiset.map_traverse

added theorem Multiset.naturality

added theorem Multiset.pure_def

added def Multiset.traverse

added theorem Multiset.traverse_map