toFinsupp_toMultiset

Mathlib.Data.Finsupp.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.toFinsupp_toMultiset

English

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

Русский

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

LaTeX

$$$\mathrm{toMultiset}(\mathrm{toFinsupp}(s)) = s$$$

Lean4

@[simp]
theorem toFinsupp_toMultiset (s : Multiset α) : Finsupp.toMultiset (toFinsupp s) = s :=
  Multiset.toFinsupp.symm_apply_apply s

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru