foldlm_toList

Mathlib.Control.Fold

URI: https://scilib.ai/kg/mathlib#Traversable.foldlm_toList

Lean4

theorem foldlm_toList {f : α → β → m α} {x : α} {xs : t β} : foldlm f x xs = List.foldlM f x (toList xs) :=
  calc
    foldlm f x xs
    _ = unop (foldlM.ofFreeMonoid f (FreeMonoid.ofList <| toList xs)) x := by
      simp only [foldlm, toList_spec, foldMap_hom_free (foldlM.ofFreeMonoid f), foldlm.ofFreeMonoid_comp_of, foldlM.get,
        FreeMonoid.ofList_toList]
    _ = List.foldlM f x (toList xs) := by simp [foldlM.ofFreeMonoid, unop_op, flip]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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