mathlib3 documentation


Equivalence between multiset and -valued finitely supported functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This defines dfinsupp.to_multiset the equivalence between Π₀ a : α, ℕ and multiset α, along with multiset.to_dfinsupp the reverse equivalence.

Note that this provides a computable alternative to finsupp.to_multiset.

@[protected, instance]
def dfinsupp.add_zero_class' {α : Type u_1} {β : Type u_2} [add_zero_class β] :
add_zero_class (Π₀ (a : α), β)

Non-dependent special case of dfinsupp.add_zero_class to help typeclass search.

def multiset.to_dfinsupp {α : Type u_1} [decidable_eq α] :
multiset α →+ Π₀ (a : α),

A computable version of multiset.to_finsupp

theorem multiset.to_dfinsupp_apply {α : Type u_1} [decidable_eq α] (s : multiset α) (a : α) :
def multiset.equiv_dfinsupp {α : Type u_1} [decidable_eq α] :
multiset α ≃+ Π₀ (a : α),

multiset.to_dfinsupp as an add_equiv.