derivative_expand — Mathlib

English

The derivative of expanded f by p satisfies a product rule with X^{p-1}:

Русский

Производная от расширенного по p полинома удовлетворяет правилу произведения с X^{p-1}:

LaTeX

$$$\operatorname{derivative}(\operatorname{expand}(R,p) f) = \operatorname{expand}(R,p)(\operatorname{derivative} f) \cdot \bigl(p \cdot X^{p-1}\bigr)$$$

Lean4

theorem derivative_expand (f : R[X]) :
    Polynomial.derivative (expand R p f) = expand R p (Polynomial.derivative f) * (p * (X ^ (p - 1) : R[X])) := by
  rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_natCast, derivative_X, mul_one]

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