log_exp_exists — Mathlib

English

For any complex z, there exists an integer n such that log(exp z) = z + n·(2πi).

Русский

Для любого комплексного числа z существует целое n такое, что log(exp z) = z + n·(2πi).

LaTeX

$$$\forall z \in \mathbb{C},\ \exists n \in \mathbb{Z},\ log(\exp z) = z + n \cdot (2 \pi i)$$$

Lean4

theorem log_exp_exists (z : ℂ) : ∃ n : ℤ, log (exp z) = z + n * (2 * π * I) :=
  by
  rw [← exp_eq_exp_iff_exists_int, exp_log]
  exact exp_ne_zero z

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