iterate_derivative_smul — Mathlib

English

For any natural k, the kth iterate of the derivative commutes with scalar multiplication: derivative^[k](s · p) = s · derivative^[k] p.

Русский

Для любого натурального k кратная итерация производной коммутирует со скаляром: D^k(s · p) = s · D^k(p).

LaTeX

$$$\operatorname{derivative}^{k}(s \cdot p) = s \cdot \operatorname{derivative}^{k}(p)$$$

Lean4

@[simp]
theorem iterate_derivative_smul {S : Type*} [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : R[X]) (k : ℕ) :
    derivative^[k] (s • p) = s • derivative^[k] p := by
  induction k generalizing p with
  | zero => simp
  | succ k ih => simp [ih]

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