sumIDeriv_C

Mathlib.Algebra.Polynomial.SumIteratedDerivative

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

← MathLib Explorer

English

The sumIDeriv of a constant polynomial C(a) is itself C(a).

Русский

Сумма повторных производных константного полинома C(a) равна самому C(a).

LaTeX

$$@[simp] sumIDeriv (C a) = C a$$

Lean4

@[simp]
theorem sumIDeriv_C (a : R) : sumIDeriv (C a) = C a := by
  rw [sumIDeriv_apply, natDegree_C, zero_add, sum_range_one, Function.iterate_zero_apply]

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

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

Разделы

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

Аффилиация

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