prod_univ_def — Mathlib

English

The product over i of f i with i ranging over Fin n equals the product of the values f i indexed by Fin n, i.e., the universal product equals the finite product over i.

Русский

Произведение по i в Fin n от f(i) равно произведению значений f i по индексу Fin n.

LaTeX

$$$\prod_{i} f(i) = \prod_{i: Fin n} f(i)$$$

Lean4

@[to_additive]
theorem prod_univ_def (f : Fin n → M) : ∏ i, f i = ((List.finRange n).map f).prod := by
  rw [← List.ofFn_eq_map, prod_ofFn]

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