hasDerivAt_zpow — Mathlib

English

For any m and x with x ≠ 0 or m ≥ 0, the derivative of x^m at x is (m) x^{m−1}.

Русский

Для любого m и x при условии x ≠ 0 или m ≥ 0 производная от x^m в точке x равна m x^{m−1}.

LaTeX

$$$x \\neq 0 \\lor 0 \\le m \\Rightarrow \\operatorname{HasDerivAt} (\\lambda t, t^m) ((m:\\\\mathbb{K}) \\cdot x^{m-1})\, x$$$

Lean4

theorem hasDerivAt_zpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) : HasDerivAt (fun x => x ^ m) ((m : 𝕜) * x ^ (m - 1)) x :=
  (hasStrictDerivAt_zpow m x h).hasDerivAt

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