exp_eq_exp_iff_exists_int — Mathlib

English

For complex numbers x and y, exp x = exp y if and only if there exists an integer n with x = y + n·(2πi).

Русский

Для комплексных чисел x и y верно: exp x = exp y тогда и только тогда, когда существует целое n, такое что x = y + n·(2πi).

LaTeX

$$$\exp x = \exp y \iff \exists n \in \mathbb{Z},\ x = y + n \cdot (2 \pi i)$$$

Lean4

theorem exp_eq_exp_iff_exists_int {x y : ℂ} : exp x = exp y ↔ ∃ n : ℤ, x = y + n * (2 * π * I) := by
  simp only [exp_eq_exp_iff_exp_sub_eq_one, exp_eq_one_iff, sub_eq_iff_eq_add']

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