prod_map_pow — Mathlib

English

For a multiset m and functions f,g on index set, the product of f(i)g(i) over i equals the product of f(i) times the product of g(i): prod(m.map (i => f i * g i)) = prod(m.map f) · prod(m.map g).

Русский

Для мультимножества m и функций f,g: произведение f(i)g(i) по i равно произведению f(i) по i умноженному на произведение g(i) по i.

LaTeX

$$$ \mathrm{prod}(\mathrm{map}(i \mapsto f(i) \cdot g(i))\, m) = \mathrm{prod}(\mathrm{map} f\, m) \cdot \mathrm{prod}(\mathrm{map} g\, m) $$$

Lean4

@[to_additive]
theorem prod_map_pow {n : ℕ} : (m.map fun i => f i ^ n).prod = (m.map f).prod ^ n :=
  m.prod_hom' (powMonoidHom n : M →* M) f

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