English
The product over Fin n equals the product over range n for a function f: Nat → α, i.e., ∏ i: Fin n, f i = ∏ i ∈ range n, f i.
Русский
Произведение по Fin n равносильно произведению по range n для функции f: Nat → α.
LaTeX
$$$\\prod_{i : \\mathrm{Fin} n} f(i) = \\prod_{i \\in \\mathrm{range}\\ n} f(i)$$$
Lean4
/-- It is equivalent to compute the product of a function over `Fin n` or `Finset.range n`. -/
@[to_additive /-- It is equivalent to sum a function over `fin n` or `finset.range n`. -/
]
theorem prod_univ_eq_prod_range [CommMonoid α] (f : ℕ → α) (n : ℕ) : ∏ i : Fin n, f i = ∏ i ∈ range n, f i :=
calc
∏ i : Fin n, f i = ∏ i : { x // x ∈ range n }, f i :=
Fintype.prod_equiv (Fin.equivSubtype.trans (Equiv.subtypeEquivRight (by simp))) _ _ (by simp)
_ = ∏ i ∈ range n, f i := by rw [← attach_eq_univ, prod_attach]
