foldl_toList

Mathlib.Control.Fold

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

Lean4

theorem foldl_toList (f : α → β → α) (xs : t β) (x : α) : foldl f x xs = List.foldl f x (toList xs) :=
  by
  rw [← FreeMonoid.toList_ofList (toList xs), ← foldl.unop_ofFreeMonoid]
  simp only [foldl, toList_spec, foldMap_hom_free, foldl.ofFreeMonoid_comp_of, Foldl.get, FreeMonoid.ofList_toList]

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

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

Разделы

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

Аффилиация

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