# Equivalence between Multiset and ℕ-valued finitely supported functions #

This defines DFinsupp.toMultiset the equivalence between Π₀ a : α, ℕ and Multiset α, along with Multiset.toDFinsupp the reverse equivalence.

instance DFinsupp.addZeroClass' {α : Type u_1} {β : Type u_3} [] :
AddZeroClass (Π₀ (x : α), β)

Non-dependent special case of DFinsupp.addZeroClass to help typeclass search.

Equations
def DFinsupp.toMultiset {α : Type u_1} [] :
(Π₀ (x : α), ) →+

A DFinsupp version of Finsupp.toMultiset.

Equations
Instances For
@[simp]
theorem DFinsupp.toMultiset_single {α : Type u_1} [] (a : α) (n : ) :
DFinsupp.toMultiset () =
def Multiset.toDFinsupp {α : Type u_1} [] :
→+ Π₀ (x : α),

A DFinsupp version of Multiset.toFinsupp.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Multiset.toDFinsupp_apply {α : Type u_1} [] (s : ) (a : α) :
(Multiset.toDFinsupp s) a =
@[simp]
theorem Multiset.toDFinsupp_support {α : Type u_1} [] (s : ) :
DFinsupp.support (Multiset.toDFinsupp s) =
@[simp]
theorem Multiset.toDFinsupp_replicate {α : Type u_1} [] (a : α) (n : ) :
Multiset.toDFinsupp () =
@[simp]
theorem Multiset.toDFinsupp_singleton {α : Type u_1} [] (a : α) :
Multiset.toDFinsupp {a} =
@[simp]
theorem Multiset.equivDFinsupp_symm_apply {α : Type u_1} [] (a : Π₀ (x : α), ) :
(AddEquiv.symm Multiset.equivDFinsupp) a = DFinsupp.toMultiset a
@[simp]
theorem Multiset.equivDFinsupp_apply {α : Type u_1} [] (a : ) :
Multiset.equivDFinsupp a = Multiset.toDFinsupp a
def Multiset.equivDFinsupp {α : Type u_1} [] :
≃+ Π₀ (x : α),

Multiset.toDFinsupp as an AddEquiv.

Equations
Instances For
@[simp]
theorem Multiset.toDFinsupp_toMultiset {α : Type u_1} [] (s : ) :
DFinsupp.toMultiset (Multiset.toDFinsupp s) = s
theorem Multiset.toDFinsupp_injective {α : Type u_1} [] :
Function.Injective Multiset.toDFinsupp
@[simp]
theorem Multiset.toDFinsupp_inj {α : Type u_1} [] {s : } {t : } :
Multiset.toDFinsupp s = Multiset.toDFinsupp t s = t
@[simp]
theorem Multiset.toDFinsupp_le_toDFinsupp {α : Type u_1} [] {s : } {t : } :
Multiset.toDFinsupp s Multiset.toDFinsupp t s t
@[simp]
theorem Multiset.toDFinsupp_lt_toDFinsupp {α : Type u_1} [] {s : } {t : } :
Multiset.toDFinsupp s < Multiset.toDFinsupp t s < t
@[simp]
theorem Multiset.toDFinsupp_inter {α : Type u_1} [] (s : ) (t : ) :
Multiset.toDFinsupp (s t) = Multiset.toDFinsupp s Multiset.toDFinsupp t
@[simp]
theorem Multiset.toDFinsupp_union {α : Type u_1} [] (s : ) (t : ) :
Multiset.toDFinsupp (s t) = Multiset.toDFinsupp s Multiset.toDFinsupp t
@[simp]
theorem DFinsupp.toMultiset_toDFinsupp {α : Type u_1} [] (f : Π₀ (x : α), ) :
Multiset.toDFinsupp (DFinsupp.toMultiset f) = f
theorem DFinsupp.toMultiset_injective {α : Type u_1} [] :
Function.Injective DFinsupp.toMultiset
@[simp]
theorem DFinsupp.toMultiset_inj {α : Type u_1} [] {f : Π₀ (_a : α), } {g : Π₀ (_a : α), } :
DFinsupp.toMultiset f = DFinsupp.toMultiset g f = g
@[simp]
theorem DFinsupp.toMultiset_le_toMultiset {α : Type u_1} [] {f : Π₀ (_a : α), } {g : Π₀ (_a : α), } :
DFinsupp.toMultiset f DFinsupp.toMultiset g f g
@[simp]
theorem DFinsupp.toMultiset_lt_toMultiset {α : Type u_1} [] {f : Π₀ (_a : α), } {g : Π₀ (_a : α), } :
DFinsupp.toMultiset f < DFinsupp.toMultiset g f < g
@[simp]
theorem DFinsupp.toMultiset_inf {α : Type u_1} [] (f : Π₀ (_a : α), ) (g : Π₀ (_a : α), ) :
DFinsupp.toMultiset (f g) = DFinsupp.toMultiset f DFinsupp.toMultiset g
@[simp]
theorem DFinsupp.toMultiset_sup {α : Type u_1} [] (f : Π₀ (_a : α), ) (g : Π₀ (_a : α), ) :
DFinsupp.toMultiset (f g) = DFinsupp.toMultiset f DFinsupp.toMultiset g