English
If s is a finite set and f: α → M with f(a) ≠ 0 for a ∈ s, and g: α → M → N with g(a,0)=1, then the product over onFinset s of f and g equals the product over a ∈ s of g(a, f(a)).
Русский
Если s — конечное множество, f: α → M с f(a) ≠ 0 для a ∈ s, и g: α → M → N с g(a,0)=1, то произведение на onFinset s равно произведению по a ∈ s: g(a, f(a)).
LaTeX
$$$$ (\\mathrm{onFinset}\\, s\, f\, hf).prod\, g = \\prod_{a \\in s} g(a, f(a)) $$$$
Lean4
/-- If `g` maps a second argument of 0 to 1, then multiplying it over the
result of `onFinset` is the same as multiplying it over the original `Finset`. -/
@[to_additive /-- If `g` maps a second argument of 0 to 0, summing it over the
result of `onFinset` is the same as summing it over the original `Finset`. -/
]
theorem onFinset_prod {s : Finset α} {f : α → M} {g : α → M → N} (hf : ∀ a, f a ≠ 0 → a ∈ s) (hg : ∀ a, g a 0 = 1) :
(onFinset s f hf).prod g = ∏ a ∈ s, g a (f a) :=
Finset.prod_subset support_onFinset_subset <| by simp +contextual [*]
