smul_finsum_mem — Mathlib

English

Let f: γ → N and s a finite set. The scalar action commutes with finsum over s: r • finsum x∈s f x = finsum x∈s r • f x.

Русский

Пусть f: γ → N и s конечное множество. Действие скаляра r над finsum над s равно finsum над s от r • f x.

LaTeX

$$$\\forall {N} {\\gamma} [\\mathsf{AddCommMonoid} N] [\\mathsf{DistribSMul} M N] {r:M} {f:\\gamma\\to N} {s: \\mathsf{Set} \\gamma},\\; finsum x\\in s f x$$

Lean4

theorem smul_finsum_mem {f : γ → N} {s : Set γ} (hs : s.Finite) : r • ∑ᶠ x ∈ s, f x = ∑ᶠ x ∈ s, r • f x :=
  (DistribSMul.toAddMonoidHom N r).map_finsum_mem f hs

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