prod_map_mul — Mathlib

English

For l : List ι and f,g : ι → M with (CommMonoid M), the product of pairwise products equals the product of the maps: (l.map (i ↦ f i * g i)).prod = (l.map f).prod * (l.map g).prod.

Русский

Для списка l и функций f,g: ι→M выполняется равенство: произведение попарных произведений равно произведению двух отдельных произведений.

LaTeX

$$$$ \\left(\\,l.map (\\lambda i \\,\\to f(i) * g(i)\\,).prod\\right) = (l.map f).prod \\cdot (l.map g).prod. $$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_map_mul {M : Type*} [CommMonoid M] {l : List ι} {f g : ι → M} :
    (l.map fun i => f i * g i).prod = (l.map f).prod * (l.map g).prod :=
  l.prod_hom₂ (· * ·) mul_mul_mul_comm (mul_one _) _ _

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