English
In a DivisionCommMonoid G, for finite s and functions f,g: α → G, the finite product distributes over division: ∏_{i∈s} f(i)/g(i) = (∏_{i∈s} f(i)) / (∏_{i∈s} g(i)).
Русский
В DivisionCommMonoid G для конечного множества s и функций f,g: α → G выполняется распределение деления по произведению: ∏_{i∈s} f(i)/g(i) = (\prod_{i∈s} f(i)) / (\prod_{i∈s} g(i)).
LaTeX
$$\operatorname{Finite}(s) \Rightarrow \prod_{i \in s} \frac{f(i)}{g(i)} = \frac{\prod_{i \in s} f(i)}{\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` divided by 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` minus the sum of `g i` over `i ∈ s`. -/
]
theorem finprod_mem_div_distrib [DivisionCommMonoid G] (f g : α → G) (hs : s.Finite) :
∏ᶠ i ∈ s, f i / g i = (∏ᶠ i ∈ s, f i) / ∏ᶠ i ∈ s, g i := by
simp only [div_eq_mul_inv, finprod_mem_mul_distrib hs, finprod_mem_inv_distrib g hs]
