derivative_add

Mathlib.Algebra.Polynomial.Derivative

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

English

The derivative of the constant polynomial 1 is 0.

Русский

Производная константы 1 равна 0.

LaTeX

$$$\\operatorname{derivative}(1) = 0.$$$

Lean4

@[simp]
theorem derivative_add {f g : R[X]} : derivative (f + g) = derivative f + derivative g :=
  derivative.map_add f g

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

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

Разделы

Аффилиация

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