hasDerivAt_pow

Mathlib.Analysis.Calculus.Deriv.Pow

URI: https://scilib.ai/kg/mathlib#hasDerivAt_pow

← MathLib Explorer

English

The derivative of x^n is n x^{n-1}.

Русский

Производная x^n равна n x^{n-1}.

LaTeX

$$$HasDerivAt\\ (fun x => x^n)\\ (n \\cdot x^{n-1})\\ x$$$

Lean4

theorem hasDerivAt_pow (n : ℕ) (x : 𝕜) : HasDerivAt (fun x : 𝕜 => x ^ n) ((n : 𝕜) * x ^ (n - 1)) x := by
  simpa using (hasStrictDerivAt_pow n x).hasDerivAt

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

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

Разделы

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

Аффилиация

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