smul_sum — Mathlib

English

The scalar multiple of the sum equals the sum of the scalars applied termwise.

Русский

Скалярное умножение суммы равно сумме скалярного умножения по каждому слагаемому.

LaTeX

$$$ b \cdot p.sum f = p.sum (\lambda n a. b \cdot f n a)$$$

Lean4

protected theorem smul_sum {S T : Type*} [AddCommMonoid S] [DistribSMul T S] (p : R[X]) (b : T) (f : ℕ → R → S) :
    b • p.sum f = p.sum fun n a => b • f n a :=
  Finsupp.smul_sum

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