sumIDeriv_eq_self_add — Mathlib

English

For any p ∈ R[X], sumIDeriv p equals p plus the derivative of sumIDeriv p: sumIDeriv p = p + derivative(sumIDeriv p).

Русский

Пусть p ∈ R[X]. Тогда sumIDeriv p = p + derivative(sumIDeriv p).

LaTeX

$$$$ \operatorname{sumIDeriv}(p) = p + \operatorname{derivative}(\operatorname{sumIDeriv}(p)) $$$$

Lean4

theorem sumIDeriv_eq_self_add (p : R[X]) : sumIDeriv p = p + derivative (sumIDeriv p) :=
  by
  rw [sumIDeriv_apply, derivative_sum, sum_range_succ', sum_range_succ, add_comm, ← add_zero (Finset.sum _ _)]
  simp_rw [← Function.iterate_succ_apply' derivative, Nat.succ_eq_add_one, Function.iterate_zero_apply,
    iterate_derivative_eq_zero (Nat.lt_succ_self _)]

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