# mathlib3documentation

data.dfinsupp.multiset

# 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 (Π₀ (a : α), β)

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

Equations
def dfinsupp.to_multiset {α : Type u_1} [decidable_eq α] :
(Π₀ (a : α), ) →+

A computable version of finsupp.to_multiset.

Equations
@[simp]
theorem dfinsupp.to_multiset_single {α : Type u_1} [decidable_eq α] (a : α) (n : ) :
def multiset.to_dfinsupp {α : Type u_1} [decidable_eq α] :
→+ Π₀ (a : α),

A computable version of multiset.to_finsupp

Equations
@[simp]
theorem multiset.to_dfinsupp_apply {α : Type u_1} [decidable_eq α] (s : multiset α) (a : α) :
=
@[simp]
theorem multiset.to_dfinsupp_support {α : Type u_1} [decidable_eq α] (s : multiset α) :
@[simp]
theorem multiset.to_dfinsupp_replicate {α : Type u_1} [decidable_eq α] (a : α) (n : ) :
@[simp]
theorem multiset.to_dfinsupp_singleton {α : Type u_1} [decidable_eq α] (a : α) :
def multiset.equiv_dfinsupp {α : Type u_1} [decidable_eq α] :
≃+ Π₀ (a : α),

multiset.to_dfinsupp as an add_equiv.

Equations
@[simp]
theorem multiset.equiv_dfinsupp_apply {α : Type u_1} [decidable_eq α] (ᾰ : multiset α) :
@[simp]
theorem multiset.equiv_dfinsupp_symm_apply {α : Type u_1} [decidable_eq α] (ᾰ : Π₀ (a : α), ) :
@[simp]
theorem multiset.to_dfinsupp_to_multiset {α : Type u_1} [decidable_eq α] (s : multiset α) :
@[simp]
theorem multiset.to_dfinsupp_inj {α : Type u_1} [decidable_eq α] {s t : multiset α} :
@[simp]
theorem multiset.to_dfinsupp_le_to_dfinsupp {α : Type u_1} [decidable_eq α] {s t : multiset α} :
@[simp]
theorem multiset.to_dfinsupp_lt_to_dfinsupp {α : Type u_1} [decidable_eq α] {s t : multiset α} :
@[simp]
theorem multiset.to_dfinsupp_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :
@[simp]
theorem multiset.to_dfinsupp_union {α : Type u_1} [decidable_eq α] (s t : multiset α) :
@[simp]
theorem dfinsupp.to_multiset_to_dfinsupp {α : Type u_1} [decidable_eq α] {f : Π₀ (a : α), } :
@[simp]
theorem dfinsupp.to_multiset_inj {α : Type u_1} [decidable_eq α] {f g : Π₀ (a : α), } :
@[simp]
theorem dfinsupp.to_multiset_le_to_multiset {α : Type u_1} [decidable_eq α] {f g : Π₀ (a : α), } :
@[simp]
theorem dfinsupp.to_multiset_lt_to_multiset {α : Type u_1} [decidable_eq α] {f g : Π₀ (a : α), } :
@[simp]
theorem dfinsupp.to_multiset_inf {α : Type u_1} [decidable_eq α] (f g : Π₀ (a : α), ) :
@[simp]
theorem dfinsupp.to_multiset_sup {α : Type u_1} [decidable_eq α] (f g : Π₀ (a : α), ) :