derivative_eval — Mathlib

English

For p = ∑ a_n X^n, the derivative evaluated at x equals ∑ a_n · n · x^{n−1}.

Русский

Для многочлена p = ∑ a_n X^n и любого x, производная(p) при подстановке x равна ∑ a_n n x^{n−1}.

LaTeX

$$$\operatorname{derivative\,eval}\_x(p) = \sum_{n\ge 0} a_n \cdot n \cdot x^{n-1}$$$

Lean4

theorem derivative_eval (p : R[X]) (x : R) : p.derivative.eval x = p.sum fun n a => a * n * x ^ (n - 1) := by
  simp_rw [derivative_apply, eval_sum, eval_mul_X_pow, eval_C]

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