English
For a list l of elements of M, folding along the map ι_Q and multiplying the results yields the standard List.foldr result, i.e., foldr Q f hf n (l.map ι_Q).prod = List.foldr (fun m n => f m n) n l.
Русский
Для списка l объектов M свёртка по генераторам ι_Q даёт результат, равный обычному списковому свёртыванию: foldr Q f hf n (l.map ι_Q).prod = List.foldr (λ m n, f m n) n l.
LaTeX
$$$foldr_Q\ \,f\ hf\ n\\,(\\,l.map\\,\\iota_Q\\,).prod = List.foldr (\\lambda m n, f\\,m\\,n)\\ n \\ l$$$
Lean4
/-- This lemma demonstrates the origin of the `foldr` name. -/
theorem foldr_prod_map_ι (l : List M) (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) :
foldr Q f hf n (l.map <| ι Q).prod = List.foldr (fun m n => f m n) n l := by
induction l with
| nil => rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]
| cons hd tl ih => rw [List.map_cons, List.prod_cons, List.foldr_cons, foldr_mul, foldr_ι, ih]
