iterate_derivative_X

Mathlib.Algebra.Polynomial.Derivative

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

English

For any k with 1 < k, the kth iterate of the derivative of the indeterminate X is zero.

Русский

Для любого k > 1, k-я производная от X равна нулю.

LaTeX

$$$\operatorname{derivative}^{k}(X) = 0$ for 1 < k$$

Lean4

@[simp]
theorem iterate_derivative_X {k} (h : 1 < k) : derivative^[k] (X : R[X]) = 0 :=
  iterate_derivative_eq_zero <| natDegree_X_le.trans_lt h

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

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

Разделы

Аффилиация

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