toMultiset_toFinsupp — Mathlib

English

The composition toMultiset ∘ toFinsupp is the identity on Multiset α: Multiset.toFinsupp (Finsupp.toMultiset f) = f.

Русский

Компоновка toMultiset ∘ toFinsupp является тождеством на Multiset α: Multiset.toFinsupp (Finsupp.toMultiset f) = f.

LaTeX

$$$\mathrm{Multiset.toFinsupp}(\mathrm{Finsupp.toMultiset}(f)) = f$$$

Lean4

@[simp]
theorem toMultiset_toFinsupp [DecidableEq α] (f : α →₀ ℕ) : Multiset.toFinsupp (Finsupp.toMultiset f) = f :=
  Multiset.toFinsupp.apply_symm_apply _

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