English
For finite index type ι, v.prod f equals the product over i of f i (equivFunOnFintype v i).
Русский
Для конечного множества индексов ι, произведение v по f равно произведению по i от f i (equivFunOnFintype v i).
LaTeX
$$$v.prod f = \\prod i, f i (DFinsupp.equivFunOnFintype v i)$$$
Lean4
@[to_additive (attr := simp)]
theorem prod_eq_prod_fintype [Fintype ι] [∀ i, Zero (β i)] [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ]
(v : Π₀ i, β i) {f : ∀ i, β i → γ} (hf : ∀ i, f i 0 = 1) : v.prod f = ∏ i, f i (DFinsupp.equivFunOnFintype v i) :=
by
suffices (∏ i ∈ v.support, f i (v i)) = ∏ i, f i (v i) by simp [DFinsupp.prod, this]
apply Finset.prod_subset v.support.subset_univ
intro i _ hi
rw [mem_support_iff, not_not] at hi
rw [hi, hf]
