derivative_sub — Mathlib

English

For polynomials f and g, the derivative of f − g is the difference of their derivatives: d(f − g) = df − dg.

Русский

Для многочленов f и g производная от f − g равна разности производных: d(f − g) = df − dg.

LaTeX

$$$\operatorname{derivative}(f - g) = \operatorname{derivative}(f) - \operatorname{derivative}(g)$$$

Lean4

@[simp]
theorem derivative_sub {f g : R[X]} : derivative (f - g) = derivative f - derivative g :=
  LinearMap.map_sub derivative f g

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