prod_eq_foldl — Mathlib

English

For a list l of elements in a monoid M, the product over l equals the fold of multiplication: l.prod = foldl (•) 1 l.

Русский

Для списка l элементов в моноиде M произведение элементов равно свёртке умножения: l.prod = foldl (•) 1 l.

LaTeX

$$$$\\text{If } l = [a_1,\\dots,a_n],\\; a_1 a_2 \\cdots a_n = \\big(\\cdots((a_1 a_2) a_3) \\cdots a_n\\big). $$$$

Lean4

@[to_additive]
theorem prod_eq_foldl : ∀ {l : List M}, l.prod = foldl (· * ·) 1 l
  | [] => rfl
  | cons a l => by
    rw [prod_cons, prod_eq_foldl, ← foldl_assoc (α := M) (op := (· * ·))]
    simp

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