English
Let c be a function from Fin n to a commutative monoid β. Then the product over all i in Fin n of c(i) equals the product over i from 0 to n−1 of c(⟨i, i < n⟩). Equivalently, ∏_{i: Fin n} c(i) = ∏_{i=0}^{n−1} c(⟨i, i< n⟩).
Русский
Пусть c: Fin n → β, где β — коммутативный моноид. Тогда произведение по всем i ∈ Fin n равно произведению по i от 0 до n−1: ∏_{i: Fin n} c(i) = ∏_{i=0}^{n−1} c(⟨i, i < n⟩).
LaTeX
$$$ \\displaystyle \\prod_{i : \\mathrm{Fin}(n)} c(i) = \\prod_{i=0}^{n-1} c\\big( \\langle i, i < n \\rangle \\big). $$$
Lean4
@[to_additive]
theorem prod_fin_eq_prod_range [CommMonoid β] {n : ℕ} (c : Fin n → β) :
∏ i, c i = ∏ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 1 :=
by
rw [← Fin.prod_univ_eq_prod_range, Finset.prod_congr rfl]
rintro ⟨i, hi⟩ _
simp only [hi, dif_pos]
