prod_mul_distrib — Mathlib

English

Distributes as a product over a set, i.e., the product of pairwise products equals the product of products.

Русский

Распределение произведения: произведение по x∈s f x * g x равно произведению по x∈s f x и по x∈s g x.

LaTeX

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

Lean4

@[to_additive]
theorem prod_mul_distrib : ∏ x ∈ s, f x * g x = (∏ x ∈ s, f x) * ∏ x ∈ s, g x :=
  Eq.trans (by rw [one_mul]; rfl) fold_op_distrib

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