iterate_derivative_intCast_mul — Mathlib

English

For any integer n and natural k, derivative iterated k times of (n) · f equals n · derivative iterated k times of f.

Русский

Для любого целого n и натурального k, k-кратно производная от (n)·f равна n · k-кратно производной от f.

LaTeX

$$$\operatorname{derivative}^{[k]}((n : R[X]) \cdot f) = n \cdot \operatorname{derivative}^{[k]}(f)$$$

Lean4

@[simp]
theorem iterate_derivative_intCast_mul {n : ℤ} {k : ℕ} {f : R[X]} :
    derivative^[k] ((n : R[X]) * f) = n * derivative^[k] f := by induction k generalizing f <;> simp [*]

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