derivative_monomial

Mathlib.Algebra.Polynomial.Derivative

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

← MathLib Explorer

English

The derivative of the monomial a X^n is a n X^{n-1} (with a ∈ R).

Русский

Производная мономиала a X^n равна a n X^{n-1}.

LaTeX

$$$\\operatorname{derivative}(\\operatorname{monomial}(n,a)) = \\operatorname{monomial}(n-1, a\\,n).$$$

Lean4

theorem derivative_monomial (a : R) (n : ℕ) : derivative (monomial n a) = monomial (n - 1) (a * n) :=
  by
  rw [derivative_apply, sum_monomial_index, C_mul_X_pow_eq_monomial]
  simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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