English
For a finite set s, the finprod of f(i)g(i) equals the product of finprod f and finprod g.
Русский
Для конечного множества s: ∏ᶠ f(i)g(i) = (∏ᶠ f(i)) (∏ᶠ g(i)).
LaTeX
$$$\\displaystyle \\prod\\ᶠ i \\in s, f(i) \\cdot g(i) = (\\prod\\ᶠ i \\in s, f(i)) \\cdot (\\prod\\ᶠ i \\in s, g(i))$$$
Lean4
/-- Given a finite set `s`, the product of `f i * g i` over `i ∈ s` equals the product of `f i`
over `i ∈ s` times the product of `g i` over `i ∈ s`. -/
@[to_additive /-- Given a finite set `s`, the sum of `f i + g i` over `i ∈ s` equals the sum of `f i`
over `i ∈ s` plus the sum of `g i` over `i ∈ s`. -/
]
theorem finprod_mem_mul_distrib (hs : s.Finite) : ∏ᶠ i ∈ s, f i * g i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ s, g i :=
finprod_mem_mul_distrib' (hs.inter_of_left _) (hs.inter_of_left _)
