iterate_derivative_C

Mathlib.Algebra.Polynomial.Derivative

URI: https://scilib.ai/kg/mathlib#Polynomial.iterate_derivative_C

English

For any a ∈ R, p ∈ R[X], and k ∈ ℕ, derivative^[k](C a · p) = C a · derivative^[k] p.

Русский

Для любого a ∈ R, p ∈ R[X] и k ∈ ℕ, D^k(C a · p) = C a · D^k p.

LaTeX

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

Lean4

@[simp]
theorem iterate_derivative_C {k} (h : 0 < k) : derivative^[k] (C a : R[X]) = 0 :=
  iterate_derivative_eq_zero <| (natDegree_C _).trans_lt h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru