mathlib documentation

data.multiset.functor

Functoriality of multiset. #

@[protected, instance]
Equations
@[simp]
theorem multiset.fmap_def {α' β' : Type u_1} {s : multiset α'} (f : α' β') :
@[protected, instance]
Equations
@[simp]
@[protected, instance]
@[simp]
theorem multiset.lift_coe {α : Type u_1} {β : Type u_2} (x : list α) (f : list α β) (h : (a b : list α), a b f a = f b) :
@[simp]
theorem multiset.map_comp_coe {α β : Type u_1} (h : α β) :
theorem multiset.id_traverse {α : Type u_1} (x : multiset α) :
theorem multiset.map_traverse {G : Type u_1 Type u_1} [applicative G] [is_comm_applicative G] {α β γ : Type u_1} (g : α G β) (h : β γ) (x : multiset α) :
theorem multiset.traverse_map {G : Type u_1 Type u_1} [applicative G] [is_comm_applicative G] {α β γ : Type u_1} (g : α β) (h : β G γ) (x : multiset α) :
theorem multiset.naturality {G H : Type u_1 Type u_1} [applicative G] [applicative H] [is_comm_applicative G] [is_comm_applicative H] (eta : applicative_transformation G H) {α β : Type u_1} (f : α G β) (x : multiset α) :