hasStrictDerivAt_cpow_const — Mathlib

English

For any x ∈ slitPlane, the derivative of z ↦ z^{c} at z = x is c x^{c-1}.

Русский

Для любого x ∈ slitPlane производная функции z ↦ z^{c} в точке z = x равна c x^{c-1}.

LaTeX

$$$\\text{If }x\\in\\mathrm{slitPlane},\\ \\dfrac{d}{dz} z^{c}\\big|_{z=x}= c\\,x^{c-1}.$$$

Lean4

theorem hasStrictDerivAt_cpow_const (h : x ∈ slitPlane) : HasStrictDerivAt (fun z : ℂ => z ^ c) (c * x ^ (c - 1)) x :=
  by simpa only [mul_zero, add_zero, mul_one] using (hasStrictDerivAt_id x).cpow (hasStrictDerivAt_const x c) h

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