iterate_derivative_map — Mathlib

English

For any polynomial p, ring hom f, and natural k, derivative^[k](p.map f) = (derivative^[k] p).map f.

Русский

Для любого p, гомоморфизма f и натурального k, k-я производная от образа p через f равна образу от k-й производной p через f.

LaTeX

$$$\operatorname{derivative}^{k}(p.map f) = (\operatorname{derivative}^{k} p).map f$$$

Lean4

@[simp]
theorem iterate_derivative_map [Semiring S] (p : R[X]) (f : R →+* S) (k : ℕ) :
    Polynomial.derivative^[k] (p.map f) = (Polynomial.derivative^[k] p).map f := by
  induction k generalizing p with
  | zero => simp
  | succ k ih => simp only [ih, Function.iterate_succ, Polynomial.derivative_map, Function.comp_apply]

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