English
For sets s, (s ∩ mulSupport f) and (s ∩ mulSupport g) finite, the finprod over s of f(i)g(i) equals the product of finprods over s of f and g separately.
Русский
Если s∩mulSupport f и s∩mulSupport g конечны, то ∏ᶠ i∈s f(i)g(i) = (∏ᶠ i∈s f(i)) (∏ᶠ i∈s g(i)).
LaTeX
$$$\\displaystyle \\left( (s \\cap mulSupport(f)).Finite \\right) \\rightarrow \\left( (s \\cap mulSupport(g)).Finite \\right) \\rightarrow \\prod\\ᶠ i \\in s, f(i) \\cdot g(i) = (\\prod\\ᶠ i \\in s, f(i)) \\cdot (\\prod\\ᶠ i \\in s, g(i))$$$
Lean4
/-- A more general version of `finprod_mem_mul_distrib` that only requires `s ∩ mulSupport f` and
`s ∩ mulSupport g` rather than `s` to be finite. -/
@[to_additive /-- A more general version of `finsum_mem_add_distrib` that only requires `s ∩ support f`
and `s ∩ support g` rather than `s` to be finite. -/
]
theorem finprod_mem_mul_distrib' (hf : (s ∩ mulSupport f).Finite) (hg : (s ∩ mulSupport g).Finite) :
∏ᶠ i ∈ s, f i * g i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ s, g i :=
by
rw [← mulSupport_mulIndicator] at hf hg
simp only [finprod_mem_def, mulIndicator_mul, finprod_mul_distrib hf hg]
