list_prod_ofFn_of_eq_dProd — Mathlib

English

For a finite n, the product of a list of DirectSum.of terms equals the DirectSum.of applied to the dProd of the indices.

Русский

Для конечного n произведение списка DirectSum.of равно DirectSum.of применяемому к dProd индексов.

LaTeX

$$$\text{List}.\text{prod} (\text{List}.\map (\\text{of } A)) = \text{of} A (\text{List}.\dProd fι fA)$$$

Lean4

theorem list_prod_ofFn_of_eq_dProd (n : ℕ) (fι : Fin n → ι) (fA : ∀ a, A (fι a)) :
    (List.ofFn fun a => of A (fι a) (fA a)).prod = of A _ ((List.finRange n).dProd fι fA) := by
  rw [List.ofFn_eq_map, ofList_dProd]

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