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 _ _