dProdIndex

Mathlib.Algebra.GradedMonoid

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

Lean4

/-- The index used by `List.dProd`. Propositionally this is equal to `(l.map fι).Sum`, but
definitionally it needs to have a different form to avoid introducing `Eq.rec`s in `List.dProd`. -/
def dProdIndex (l : List α) (fι : α → ι) : ι :=
  l.foldr (fun i b => fι i + b) 0

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

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

Разделы

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

Аффилиация

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