eval₂_eq_sum_range — Mathlib

English

A reformulation of the expansion of (1 + y)^d: (d + 1)(1 + y)^d − (d + 1) y^d = sum_{i=0}^d binom(d + 1, i) · i · y^{i - 1}.

Русский

Переформулировка разложения (1 + y)^d: (d + 1)(1 + y)^d − (d + 1) y^d = сумма_{i=0}^d {d + 1 \choose i} · i · y^{i − 1}.

LaTeX

$$$(d+1)(1+y)^d - (d+1) y^d = \\sum_{i=0}^d {d+1 \\choose i} \\cdot i \\cdot y^{i-1}$$$

Lean4

theorem eval₂_eq_sum_range : p.eval₂ f x = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i :=
  _root_.trans (congr_arg _ p.as_sum_range) (_root_.trans (eval₂_finset_sum f _ _ x) (congr_arg _ (by simp)))

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