prod_div_distrib — Mathlib

English

In a division-commutative monoid, the division distributes over a finite product: ∏_{x∈s} f(x)/g(x) = (∏_{x∈s} f(x)) / (∏_{x∈s} g(x)).

Русский

В моноиде с делением деление распределяется по конечному произведению: ∏ f(x)/g(x) = (∏ f(x)) / (∏ g(x)).

LaTeX

$$$$\prod_{x \in s} \frac{f(x)}{g(x)} = \frac{\prod_{x \in s} f(x)}{\prod_{x \in s} g(x)}.$$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_div_distrib (f g : ι → G) : ∏ x ∈ s, f x / g x = (∏ x ∈ s, f x) / ∏ x ∈ s, g x :=
  Multiset.prod_map_div

Похожие утверждения