mapDomain_finset_sum — Mathlib

English

The mapDomain distributes over finite sums indexed by a Finset.

Русский

MapDomain распределяется по конечной сумме, индексированной Finset.

LaTeX

$$$\\operatorname{mapDomain} f\\Bigl( \\sum_{i \\in s} v_i \\Bigr) = \\sum_{i \\in s} \\operatorname{mapDomain} f (v_i).$$$

Lean4

theorem mapDomain_finset_sum {f : α → β} {s : Finset ι} {v : ι → α →₀ M} :
    mapDomain f (∑ i ∈ s, v i) = ∑ i ∈ s, mapDomain f (v i) :=
  map_sum (mapDomain.addMonoidHom f) _ _

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