list_prod_ofFn_eq_dProd — Mathlib

English

For any finite n, and f: Fin n → GradedMonoid A, the product of the list of f equals the graded-mactored dProd form.

Русский

Для любой функции f: Fin n → GradedMonoid A произведение списка f эквивалентно форме dProd.

LaTeX

$$$(List.ofFn f).prod = GradedMonoid.mk _ ((List.finRange n).dProd (\\lambda i. (f i).1) (\\lambda i. (f i).2))$$$

Lean4

theorem list_prod_ofFn_eq_dProd {n : ℕ} (f : Fin n → GradedMonoid A) :
    (List.ofFn f).prod = GradedMonoid.mk _ ((List.finRange n).dProd (fun i => (f i).1) fun i => (f i).2) := by
  rw [List.ofFn_eq_map, GradedMonoid.list_prod_map_eq_dProd]

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