dProdIndex_eq_map_sum — Mathlib

English

For any list l of α and fι: α → ι, the dProdIndex of l with fι equals the sum of fι along l.

Русский

Для списка l из α и отображения fι: α → ι сумма показателей градации совпадает с dProdIndex.

LaTeX

$$$l.dProdIndex f\\u03b9 = (l.map f\\u026a).sum$$$

Lean4

theorem dProdIndex_eq_map_sum (l : List α) (fι : α → ι) : l.dProdIndex fι = (l.map fι).sum := by
  match l with
  | [] => simp
  | head :: tail => simp [List.dProdIndex_eq_map_sum tail fι]

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