sum_smul_index

Mathlib.Algebra.Polynomial.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.sum_smul_index

← MathLib Explorer

English

The sum over b times p with f equals p.sum with f evaluated at b times coefficient.

Русский

Сумма по b·p имеет вид p.sum с f(n, b·a).

LaTeX

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

Lean4

theorem sum_smul_index {S : Type*} [AddCommMonoid S] (p : R[X]) (b : R) (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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru