sum_C_index — Mathlib

English

The sum over a constant polynomial Cu is the evaluation f at the constant term: (C a).sum f = f 0 a, under suitable f.

Русский

Сумма по константному полиному Cu даёт значение f в нулевом индексе: (C a).sum f = f 0 a, при подходящих условиях на f.

LaTeX

$$$ (C a).sum f = f 0 a$ (при условии $f 0 0 = 0$)$$

Lean4

@[simp]
theorem sum_C_index {a} {β} [AddCommMonoid β] {f : ℕ → R → β} (h : f 0 0 = 0) : (C a).sum f = f 0 a :=
  sum_monomial_index a f h

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