English
If ι is AddMonoid and R is a Monoid, then the dependent product over a list l equals the ordinary product when all indexed types are the same.
Русский
Если ι — AddMonoid и R — Monoid, то зависимое произведение над списком l равно обычному произведению, когда все индексированные типы совпадают.
LaTeX
$$$@List.dProd _ _ (\\lambda _ : ι => R) _ _ l fι fA = (l.map fA).prod$$$
Lean4
/-- When all the indexed types are the same, the dependent product is just the regular product. -/
@[simp]
theorem dProd_monoid {α} [AddMonoid ι] [Monoid R] (l : List α) (fι : α → ι) (fA : α → R) :
@List.dProd _ _ (fun _ : ι => R) _ _ l fι fA = (l.map fA).prod := by
match l with
| [] =>
rw [List.dProd_nil, List.map_nil, List.prod_nil]
rfl
| head :: tail =>
rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]
rfl
