English
The complex exponential is 1 exactly at integer multiples of 2πi: exp(x) = 1 iff x = n·(2πi) for some integer n.
Русский
Экспонента на комплексной плоскости равна единице только в точках x = n·(2πi), где n ∈ ℤ.
LaTeX
$$$\exp x = 1 \iff \exists n \in \mathbb{Z},\ x = n \cdot (2 \pi i)$$$
Lean4
theorem exp_eq_one_iff {x : ℂ} : exp x = 1 ↔ ∃ n : ℤ, x = n * (2 * π * I) :=
by
constructor
· intro h
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos x.im (-π) with ⟨n, hn, -⟩
use -n
rw [Int.cast_neg, neg_mul, eq_neg_iff_add_eq_zero]
have : (x + n * (2 * π * I)).im ∈ Set.Ioc (-π) π := by simpa [two_mul, mul_add] using hn
rw [← log_exp this.1 this.2, exp_periodic.int_mul n, h, log_one]
· rintro ⟨n, rfl⟩
exact (exp_periodic.int_mul n).eq.trans exp_zero
