prod_mul_prod_comm — Mathlib

English

A commutation identity for products: the product of pointwise products equals the product of two separate products with permuted factors.

Русский

Коммутативное тождество для произведений: произведение по точечного произведения равно произведению двух отдельных произведений с перестановкой факторов.

LaTeX

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

Lean4

@[to_additive]
theorem prod_mul_prod_comm (f g h i : ι → M) :
    (∏ a ∈ s, f a * g a) * ∏ a ∈ s, h a * i a = (∏ a ∈ s, f a * h a) * ∏ a ∈ s, g a * i a := by
  simp_rw [prod_mul_distrib, mul_mul_mul_comm]

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