sum_monomial_index — Mathlib

English

Summing over a monomial returns the corresponding coefficient value.

Русский

Сумма по мономиалу возвращает соответствующее значение коэффициента.

LaTeX

$$$ \forall p, (\sum n a \mapsto monomial n a).sum f = f \text{ on the appropriate coefficient}$$$

Lean4

@[simp]
theorem sum_monomial_index {S : Type*} [AddCommMonoid S] {n : ℕ} (a : R) (f : ℕ → R → S) (hf : f n 0 = 0) :
    (monomial n a : R[X]).sum f = f n a :=
  Finsupp.sum_single_index hf

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