prod

Mathlib.Algebra.BigOperators.Group.List.Defs

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

Lean4

/-- Product of a list.

`List.prod [a, b, c] = a * (b * (c * 1))` -/
@[to_additive existing]
def prod {α} [Mul α] [One α] : List α → α :=
  foldr (· * ·) 1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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