sum_smul_index' — Mathlib

English

A generalization: for p ∈ R[X], b ∈ T, and f : ℕ → R → S, summation commutes with scalar multiplication by b.

Русский

Обобщение: сумма по p и умножение на b внутри суммы сохраняются при f.

LaTeX

$$$ (\text{instHSMul}.hSMul b p).sum f = p.sum (n a => f n (b \cdot a))$$$

Lean4

theorem sum_smul_index' {S T : Type*} [DistribSMul T R] [AddCommMonoid S] (p : R[X]) (b : T) (f : ℕ → R → S)
    (hf : ∀ i, f i 0 = 0) : (b • p).sum f = p.sum fun n a => f n (b • a) :=
  Finsupp.sum_smul_index' hf

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