ofList_smul

Mathlib.Algebra.FreeMonoid.Basic

URI: https://scilib.ai/kg/mathlib#FreeMonoid.ofList_smul

English

For f: α → β → β, l: List α and b ∈ β, ofList l • b equals l.foldr f b.

Русский

Для f: α → β → β, списка l и b ∈ β, выполняется ofList l • b = l.foldr f b.

LaTeX

$$$ ofList\ l \cdot b = l.foldr\ f\ b $$$

Lean4

@[to_additive]
theorem ofList_smul (f : α → β → β) (l : List α) (b : β) :
    haveI := mkMulAction f
    ofList l • b = l.foldr f b :=
  rfl

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

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

Разделы

Аффилиация

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