divX_X_pow

Mathlib.Algebra.Polynomial.Inductions

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

English

For any natural n, divX(X^n) = 0 if n = 0, and divX(X^n) = X^{n-1} otherwise.

Русский

Для любого натурального n: divX(X^n) = 0, если n = 0; иначе divX(X^n) = X^{n-1}.

LaTeX

$$$\\operatorname{divX}\\bigl(X^{n}\\bigr) = \\begin{cases}0, & n = 0, \\\\ X^{\,n-1}, & n > 0.\\end{cases}$$$

Lean4

theorem divX_X_pow : divX (X ^ n : R[X]) = if (n = 0) then 0 else X ^ (n - 1) :=
  by
  cases n
  · simp
  · ext n
    simp [coeff_X_pow]

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

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

Разделы

Аффилиация

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