fold_singleton

Mathlib.Data.Multiset.Fold

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

English

For any α and a, the fold of a singleton {a} with b under op equals a * b.

Русский

Для любого α и a свёртка над {a} с начальным значением b равна a · b.

LaTeX

$$$ ({ a } : Multiset α).\mathrm{fold} \ op \ b = a \cdot b $$$

Lean4

theorem fold_singleton (b a : α) : ({ a } : Multiset α).fold op b = a * b :=
  foldr_singleton _ _ _

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

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

Разделы

Аффилиация

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