sum_eq_of_subset — Mathlib

English

If f(i,0)=0 for all i and p.support ⊆ s, then p.sum f = ∑_{n∈s} f(n, coeff n).

Русский

Если f(i,0)=0 для всех i и поддержка полинома ⊆ s, то сумма по полиному равна сумме по s.

LaTeX

$$$ p.sum f = \sum_{n \in s} f(n, p.coeff(n)) \quad \text{given } (\forall i, f(i,0)=0) \text{ and } p.support \subseteq s$$$

Lean4

theorem sum_eq_of_subset {S : Type*} [AddCommMonoid S] {p : R[X]} (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0) {s : Finset ℕ}
    (hs : p.support ⊆ s) : p.sum f = ∑ n ∈ s, f n (p.coeff n) :=
  Finsupp.sum_of_support_subset _ hs f (fun i _ ↦ hf i)

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