English
Let N be aMonoid; for any function f: ι → α → N with finite mulSupport, the pointwise action equals the product of evaluations: (finprod f) a = finprod (λ i, f i a).
Русский
Пусть N — моноид; для любой функции f: ι → α → N с конечной мультиподдержкой выполняется: (finprod f) a = finprod (λ i, f i a).
LaTeX
$$$ (\\text{mulSupport } f).Finite \\\\Rightarrow (\\\\prod^\\mathrm{f} i, f i) a = \\\\prod^\\mathrm{f} i, f i a $$$
Lean4
@[to_additive (attr := simp)]
theorem finprod_apply {α ι : Type*} {f : ι → α → N} (hf : (mulSupport f).Finite) (a : α) :
(∏ᶠ i, f i) a = ∏ᶠ i, f i a := by
classical
have hf' : (mulSupport fun i ↦ f i a).Finite := hf.subset (by aesop)
simp only [finprod_def, dif_pos, hf, hf', Finset.prod_apply]
symm
apply Finset.prod_subset <;> aesop
