derivativeFun_C

Mathlib.RingTheory.PowerSeries.Derivative

URI: https://scilib.ai/kg/mathlib#PowerSeries.derivativeFun_C

English

The derivative of a constant power-series with value C r is zero.

Русский

Производная константного степенного ряда C r равна нулю.

LaTeX

$$$ \\frac{d}{dX} (C\\,r) = 0 $$$

Lean4

theorem derivativeFun_C (r : R) : derivativeFun (C r) = 0 :=
  by
  ext n
  rw [coeff_derivativeFun, coeff_succ_C, zero_mul, (coeff n).map_zero]

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

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

Разделы

Аффилиация

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