mapDomain_sum — Mathlib

English

MapDomain distributes over sums: mapDomain f (s.sum v) = s.sum (λ a b, mapDomain f (v a b)).

Русский

MapDomain распределяется по суммам: mapDomain f (s.sum v) = s.sum (λ a b, mapDomain f (v a b)).

LaTeX

$$$ mapDomain\ f\ (s.sum\ v) = s.sum\ (\lambda a b, mapDomain\ f\ (v\ a\ b)) $$$

Lean4

@[to_additive]
theorem mapDomain_sum (f : M → N) (s : MonoidAlgebra S M) (v : M → S → MonoidAlgebra R M) :
    mapDomain f (s.sum v) = s.sum fun a b ↦ mapDomain f (v a b) :=
  Finsupp.mapDomain_sum

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