English
For a list l of elements of M and a bilinear map f as above, the left-fold over the product of ι_Q images equals List.foldl with a reordered argument order: foldl Q f hf n (l.map ι_Q).prod = List.foldl (fun m n => f n m) n l.
Русский
Для списка l состоящего из M и f как выше, левая свёртка над произведением образов ι_Q равна List.foldl с переставленным порядком аргументов: foldl Q f hf n (l.map ι_Q).prod = List.foldl (fun m n => f n m) n l.
LaTeX
$$$\\foldl_Q f hf n (l.map \\lambdas ι_Q).prod = List.foldl (\\lambda m n, f\\,n\\,m) n l$$$
Lean4
/-- This lemma demonstrates the origin of the `foldl` name. -/
theorem foldl_prod_map_ι (l : List M) (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) :
foldl Q f hf n (l.map <| ι Q).prod = List.foldl (fun m n => f n m) n l := by
rw [← foldr_reverse, reverse_prod_map_ι, ← List.map_reverse, foldr_prod_map_ι, List.foldr_reverse]
