coe_fold_l — Mathlib

English

For a commutative and associative operation op, and a list l, the multiset fold over ofList l equals List.foldl: fold op b (ofList l) = List.foldl op b l.

Русский

Для коммутативной и ассоциативной операции op и списка l равны: свёртка по мультимножеству отList l равна слева свёртке списка: fold op b (ofList l) = List.foldl op b l.

LaTeX

$$$ \text{theorem } \text{coe\_fold\_l}(op)\; (b)\; (l) :\; \mathrm{fold}\ op\ b\ (\mathrm{Multiset}.\mathrm{ofList} \ l) = \mathrm{List}.\mathrm{foldl} \ op \ b \ l $$$

Lean4

theorem coe_fold_l (b : α) (l : List α) : fold op b l = l.foldl op b :=
  (coe_foldr_swap op b l).trans <| by simp [hc.comm]

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