toMultiset — Mathlib

English

There is a natural AddMonoidHom toMultiset : (Π₀ _ : α, ℕ) →+ Multiset α, sending f to the multiset where each a occurs f(a) times.

Русский

Существует естественное тождественное отображение toMultiset: (Π₀ a : α, ℕ) →+ Multiset α, отображающее f в мультимножество, где каждый элемент a встречается f(a) раз.

LaTeX

$$$$ \\operatorname{toMultiset}: (\\Pi_0 _ : \\alpha, \\mathbb{N}) \\to^+ \\operatorname{Multiset} \\alpha $$$$

Lean4

/-- A DFinsupp version of `Finsupp.toMultiset`. -/
def toMultiset : (Π₀ _ : α, ℕ) →+ Multiset α :=
  DFinsupp.sumAddHom fun a : α ↦ Multiset.replicateAddMonoidHom a

Похожие утверждения