prod_mul — Mathlib

English

The product distributes over finsupps: the product of pointwise products equals the product of the products.

Русский

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

LaTeX

$$$$ \prod_{a} (h_1(a,b) \cdot h_2(a,b)) = \left(\prod_{a} h_1(a,b)\right) \cdot \left(\prod_{a} h_2(a,b)\right). $$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_mul [Zero M] [CommMonoid N] {f : α →₀ M} {h₁ h₂ : α → M → N} :
    (f.prod fun a b => h₁ a b * h₂ a b) = f.prod h₁ * f.prod h₂ :=
  Finset.prod_mul_distrib

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