prodAux_eq — Mathlib

English

For any list l of elements of a Monoid M, FreeMonoid.prodAux l equals l.prod, i.e., the definitional fold coincides with the standard list product.

Русский

Для любого списка l элементов моноида M, FreeMonoid.prodAux l равно l.prod, то есть дефиниционная свертка совпадает с обычным произведением списка.

LaTeX

$$$\\\\forall M [Monoid M] (l : List M), \\\\; FreeMonoid.prodAux l = l.prod$$$

Lean4

@[to_additive]
theorem prodAux_eq : ∀ l : List M, FreeMonoid.prodAux l = l.prod
  | [] => rfl
  | (_ :: xs) => by simp [prodAux, List.prod_eq_foldl]

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