derivativeFun_smul — Mathlib

English

For any scalar r and power-series f, derivative(r · f) = r · derivative(f).

Русский

Для скаляра r и степенного ряда f верно: (r · f)' = r · f'.

LaTeX

$$$ \\mathrm{derivative}(r \\cdot f) = r \\cdot \\mathrm{derivative}(f) $$$

Lean4

theorem derivativeFun_smul (r : R) (f : R⟦X⟧) : derivativeFun (r • f) = r • derivativeFun f := by
  rw [smul_eq_C_mul, smul_eq_C_mul, derivativeFun_mul, derivativeFun_C, smul_zero, add_zero, smul_eq_mul]

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