hasStrictDerivAt_log — Mathlib

English

On the slit plane, the derivative of the complex logarithm is the reciprocal: d/dz log z = 1/z.

Русский

На разрезанной плоскости производная комплексного логарифма равна обратному значению: d/dz log z = 1/z.

LaTeX

$$$$ \frac{d}{dz}\log z = \frac{1}{z}, \quad z \in \mathrm{slitPlane}. $$$$

Lean4

theorem hasStrictDerivAt_log {x : ℂ} (h : x ∈ slitPlane) : HasStrictDerivAt log x⁻¹ x :=
  have h0 : x ≠ 0 := slitPlane_ne_zero h
  expPartialHomeomorph.hasStrictDerivAt_symm h h0 <| by simpa [exp_log h0] using hasStrictDerivAt_exp (log x)

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