mapDomain_sum — Mathlib

English

A generalization that mapDomain respects finsupp.sum: moving mapDomain inside the sum.

Русский

Обобщение: mapDomain сохраняет сумму finsupp, т.е. перенос внутри суммы.

LaTeX

$$$\\operatorname{mapDomain} f\\Bigl( s.sum v \\Bigr) = s.sum (\\lambda a b, \\operatorname{mapDomain} f (v a b)).$$$

Lean4

theorem mapDomain_sum [Zero N] {f : α → β} {s : α →₀ N} {v : α → N → α →₀ M} :
    mapDomain f (s.sum v) = s.sum fun a b => mapDomain f (v a b) :=
  map_finsuppSum (mapDomain.addMonoidHom f : (α →₀ M) →+ β →₀ M) _ _

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