hasStrictDerivAt_pow

Mathlib.Analysis.Calculus.Deriv.Pow

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

← MathLib Explorer

English

For any n, HasStrictDerivAt (fun x ↦ x^n) at x equals n x^{n-1}.

Русский

Для любого n имеет место HasStrictDerivAt( x^n ) в x равно n x^{n-1}.

LaTeX

$$$$\text{HasStrictDerivAt}\bigl(x\mapsto x^n,\; n\,x^{n-1},\; x\bigr). $$$$

Lean4

theorem hasStrictDerivAt_pow (n : ℕ) (x : 𝕜) : HasStrictDerivAt (fun x : 𝕜 ↦ x ^ n) (n * x ^ (n - 1)) x := by
  simpa using (hasStrictDerivAt_id x).pow n

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

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

Разделы

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

Аффилиация

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