sumIDeriv_X

Mathlib.Algebra.Polynomial.SumIteratedDerivative

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

← MathLib Explorer

English

The sumIDeriv of X equals X plus C 1.

Русский

Сумма повторных производных X равна X плюс C 1.

LaTeX

$$$sumIDeriv\ X = X + C\ 1$$$

Lean4

@[simp]
theorem sumIDeriv_X : sumIDeriv X = X + C 1 := by
  rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply, Function.iterate_one,
    derivative_X, eq_natCast, Nat.cast_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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