foldr_toList

Mathlib.Control.Fold

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

Lean4

theorem foldr_toList (f : α → β → β) (xs : t α) (x : β) : foldr f x xs = List.foldr f x (toList xs) :=
  by
  change _ = Foldr.ofFreeMonoid _ (FreeMonoid.ofList <| toList xs) _
  rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free, foldr.ofFreeMonoid_comp_of]

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

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

Разделы

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

Аффилиация

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