deriv_cpow_const — Mathlib

English

For complex x in the slit plane, the derivative of the map z ↦ z^{c} at z = x is c x^{c-1}.

Русский

Для комплексного x из разрезанной плоскости производная отображения 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 deriv_cpow_const (hx : x ∈ Complex.slitPlane) : deriv (fun (x : ℂ) ↦ x ^ c) x = c * x ^ (c - 1) :=
  (hasStrictDerivAt_cpow_const hx).hasDerivAt.deriv

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