sum_add — Mathlib

English

For p ∈ SkewMonoidAlgebra k G and f,g : G → k → S, (p.sum (n x ↦ f n x + g n x)) = p.sum f + p.sum g.

Русский

Для p и функций f,g: сумма по p от (f+n x) равна сумма по p от f плюс сумма по p от g.

LaTeX

$$$\\mathrm{sum}\\ p\\ (\\lambda n\\ x, f\\ n\\ x + g\\ n\\ x) = p.\\mathrm{sum}\\ f + p.\\mathrm{sum}\\ g$$$

Lean4

@[simp]
theorem sum_add {S : Type*} [AddCommMonoid S] (p : SkewMonoidAlgebra k G) (f g : G → k → S) :
    (p.sum fun n x ↦ f n x + g n x) = p.sum f + p.sum g :=
  Finsupp.sum_add

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