exp_eq_one — Mathlib

English

For a real number r, exp r = 1 if and only if r is an integer multiple of 2π.

Русский

Для вещественного числа r верно: exp r = 1 тогда и только тогда, когда r является целым кратным 2π.

LaTeX

$$$$ \exp r = 1 \iff \exists n \in \mathbb{Z},\ r = n\cdot(2\pi). $$$$

Lean4

theorem exp_eq_one {r : ℝ} : exp r = 1 ↔ ∃ n : ℤ, r = n * (2 * π) := by
  simp [Circle.ext_iff, Complex.exp_eq_one_iff, ← mul_assoc, Complex.I_ne_zero, ← Complex.ofReal_inj]

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