log_exp — Mathlib

English

If x ∈ ℂ with -π < Im(x) ≤ π, then log(exp x) = x.

Русский

Если x ∈ ℂ и -π < Im(x) ≤ π, то log(exp x) = x.

LaTeX

$$$\log(\exp x) = x \quad\text{when } -\pi < \operatorname{Im}(x) \le \pi.$$$

Lean4

theorem log_exp {x : ℂ} (hx₁ : -π < x.im) (hx₂ : x.im ≤ π) : log (exp x) = x := by
  rw [log, norm_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
    arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]

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