derivative_intCast

Mathlib.Algebra.Polynomial.Derivative

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

English

For any integer n, the derivative of n as a constant polynomial is zero.

Русский

Для любого целого n производная от n как константного многочлена равна нулю.

LaTeX

$$$\operatorname{derivative}(n : R[X]) = 0$$$

Lean4

@[simp]
theorem derivative_intCast {n : ℤ} : derivative (n : R[X]) = 0 :=
  by
  rw [← C_eq_intCast n]
  exact derivative_C

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

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

Разделы

Аффилиация

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