derivative_coe — Mathlib

English

The derivative of a polynomial f as a power-series equals the derivative of f as a polynomial (embedding preserves derivative).

Русский

Производная полинома f как степенного ряда равна производной f как полинома (встроение сохраняет производную).

LaTeX

$$$ (f : R\\,[X]) \\text{ как степенной ряд } \\mathrm{derivativeFun} = \\mathrm{derivative}(f) $$$

Lean4

theorem derivative_coe (f : R[X]) : d⁄dX R f = Polynomial.derivative f :=
  derivativeFun_coe f

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