pderiv_one

Mathlib.Algebra.MvPolynomial.PDeriv

URI: https://scilib.ai/kg/mathlib#MvPolynomial.pderiv_one

English

The derivative of the constant polynomial 1 with respect to any i is zero.

Русский

Производная константы 1 по любой переменной равна нулю.

LaTeX

$$$$ pderiv(i)(1) = 0. $$$$

Lean4

theorem pderiv_one {i : σ} : pderiv i (1 : MvPolynomial σ R) = 0 :=
  pderiv_C

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

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

Разделы

Аффилиация

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