dvd_iterate_derivative_pow — Mathlib

English

Let f ∈ R[X], n ∈ ℕ and m>0. Then n divides eval c of derivative^[m](f^n) for any c ∈ R.

Русский

Пусть f ∈ R[X], n ∈ ℕ и m>0. Тогда n делит eval c( derivative^[m](f^n) ) для любого c ∈ R.

LaTeX

$$$$ (n : R) \mid \mathrm{eval}_c(\operatorname{derivative}^{m}(f^{n})) $$$$

Lean4

theorem dvd_iterate_derivative_pow (f : R[X]) (n : ℕ) {m : ℕ} (c : R) (hm : m ≠ 0) :
    (n : R) ∣ eval c (derivative^[m] (f ^ n)) :=
  by
  obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm
  rw [Function.iterate_succ_apply, derivative_pow, mul_assoc, C_eq_natCast, iterate_derivative_natCast_mul, eval_mul,
    eval_natCast]
  exact dvd_mul_right _ _

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