Multiset.filterMap as an additive monoid hom

Multiset.filterMapAddMonoidHom bundles Multiset.filterMap f as an additive monoid hom, as Multiset.mapAddMonoidHom bundles Multiset.map f, so that map_sum, map_list_sum and map_nsmul apply to it. [UPSTREAM] candidate; eventual mathlib home Mathlib.Algebra.Order.Group.Multiset.

def Multiset.filterMapAddMonoidHom {α : Type u_1} {β : Type u_2} (f : α → Option β) : Multiset α →+ Multiset β

Multiset.filterMap as an AddMonoidHom.

Equations

• Multiset.filterMapAddMonoidHom f = { toFun := Multiset.filterMap f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Multiset.filterMapAddMonoidHom_apply {α : Type u_1} {β : Type u_2} (f : α → Option β) (s : Multiset α) : (filterMapAddMonoidHom f) s = filterMap f s

@[simp]

theorem Multiset.coe_filterMapAddMonoidHom {α : Type u_1} {β : Type u_2} (f : α → Option β) : ⇑(filterMapAddMonoidHom f) = filterMap f