subtypeDomain_finsupp_sum — Mathlib

English

Sum distributes over subtypeDomain similarly to the previous sum rule.

Русский

Сумма внутри подтип-домена распространяется аналогично предыдущему правилу суммы.

LaTeX

$$$$ (s.sum h).subtypeDomain p = s.sum (\\lambda c d, (h c d).subtypeDomain p). $$$$

Lean4

theorem subtypeDomain_finsupp_sum [Zero N] {s : β →₀ N} {h : β → N → α →₀ M} :
    (s.sum h).subtypeDomain p = s.sum fun c d => (h c d).subtypeDomain p :=
  subtypeDomain_sum

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