English
For finite f,g, the finprod of f(i)/g(i) equals the finprod of f(i) divided by the finprod of g(i).
Русский
Для конечных f,g: \\( \\prodᶠ f(i)/g(i) = (\\prodᶠ f(i)) / (\\prodᶠ g(i)) \\).
LaTeX
$$$\\displaystyle \\prod\\ᶠ i, \\frac{f(i)}{g(i)} = \\frac{\\prod\\ᶠ i, f(i)}{\\prod\\ᶠ i, g(i)}$$$
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` divided 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` minus the sum of `g i`. -/
]
theorem finprod_div_distrib [DivisionCommMonoid G] {f g : α → G} (hf : (mulSupport f).Finite)
(hg : (mulSupport g).Finite) : ∏ᶠ i, f i / g i = (∏ᶠ i, f i) / ∏ᶠ i, g i := by
simp only [div_eq_mul_inv, finprod_mul_distrib hf ((mulSupport_fun_inv g).symm.rec hg), finprod_inv_distrib]
