English
For a finite set s, the product of f(i)g(i) equals the product of f(i) times the product of g(i).
Русский
Для конечного множества s произведение f(i)g(i) по i равно произведению f(i) по i умноженному на произведение g(i) по i.
LaTeX
$$$\\displaystyle \\prod\\ᶠ i \\in s, f(i) \\cdot g(i) = \\left(\\prod\\ᶠ i \\in s, f(i)\\right) \\cdot \\left(\\prod\\ᶠ i \\in s, g(i)\\right)$$$
Lean4
/-- If the multiplicative supports of `f` and `g` are finite, then the product of `f i * g i` equals
the product of `f i` multiplied by the product of `g i`. -/
@[to_additive /-- If the additive supports of `f` and `g` are finite, then the sum of `f i + g i`
equals the sum of `f i` plus the sum of `g i`. -/
]
theorem finprod_mul_distrib (hf : (mulSupport f).Finite) (hg : (mulSupport g).Finite) :
∏ᶠ i, f i * g i = (∏ᶠ i, f i) * ∏ᶠ i, g i := by
classical
rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf Finset.subset_union_left,
finprod_eq_prod_of_mulSupport_toFinset_subset g hg Finset.subset_union_right, ← Finset.prod_mul_distrib]
refine finprod_eq_prod_of_mulSupport_subset _ ?_
simp only [Finset.coe_union, Finite.coe_toFinset, mulSupport_subset_iff, mem_union, mem_mulSupport]
intro x
contrapose!
rintro ⟨hf, hg⟩
simp [hf, hg]
