iterate_derivative_natCast_mul — Mathlib

English

Let R be a semiring and f ∈ R[X]. For any natural k, the k-th iterate of the derivative is linear with respect to the constant n ∈ R[X]: derivative^[k]((n : R[X]) * f) = n * derivative^[k] f.

Русский

Пусть R — полукольцо и f ∈ R[X]. Для любого натурального k итеративная производная линейна по константному многочлену n: derivative^[k]((n : R[X]) * f) = n * derivative^[k] f.

LaTeX

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

Lean4

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

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