prod_eq_foldr

Mathlib.Algebra.BigOperators.Group.List.Defs

URI: https://scilib.ai/kg/mathlib#List.prod_eq_foldr

English

For any list l over a monoid M, its product equals the fold with multiplication starting from 1: prod(l) = foldr (×) 1 l.

Русский

Для любого списка l над моноидом M произведение равно свёртке по умножению, начиная с 1: prod(l) = foldr (×) 1 l.

LaTeX

$$$l.prod = \mathrm{foldr}(\\cdot, 1, l)$$$

Lean4

@[to_additive]
theorem prod_eq_foldr {l : List M} : l.prod = foldr (· * ·) 1 l :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru