LogDeriv_exp — Mathlib

English

The logarithmic derivative of the complex exponential is the constant 1: logDeriv(Complex.exp) = 1.

Русский

Логарифмическая производная экспоненты комплексной равна константе 1: logDeriv(Complex.exp) = 1.

LaTeX

$$$\logDeriv(\mathrm{Complex}.\exp) = 1$$$

Lean4

@[simp]
theorem LogDeriv_exp : logDeriv (Complex.exp) = 1 := by
  ext
  rw [logDeriv, Complex.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]

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