sumIDeriv_derivative — Mathlib

English

For any p ∈ R[X], sumIDeriv(derivative p) = derivative(sumIDeriv p).

Русский

Для любого p ∈ R[X] выполняется sumIDeriv(derivative p) = derivative(sumIDeriv p).

LaTeX

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

Lean4

theorem sumIDeriv_derivative (p : R[X]) : sumIDeriv (derivative p) = derivative (sumIDeriv p) :=
  by
  rw [sumIDeriv_apply_of_le ((natDegree_derivative_le p).trans tsub_le_self), sumIDeriv_apply, derivative_sum]
  simp_rw [← Function.iterate_succ_apply, Function.iterate_succ_apply']

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