derivativeFun_one

Mathlib.RingTheory.PowerSeries.Derivative

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

English

The derivative of the constant polynomial 1 is zero: derivative(1) = 0.

Русский

Производная константы 1 равна нулю: derivative(1) = 0.

LaTeX

$$$ \\mathrm{derivative}(1) = 0 $$$

Lean4

theorem derivativeFun_one : derivativeFun (1 : R⟦X⟧) = 0 := by rw [← map_one C, derivativeFun_C (1 : R)]

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

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

Разделы

Аффилиация

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