exp_eq_exp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exp_eq_exp {x y : ℝ} : exp x = exp y ↔ ∃ m : ℤ, x = y + m * (2 * π) :=
  by
  rw [Subtype.ext_iff, coe_exp, coe_exp, exp_eq_exp_iff_exists_int]
  refine exists_congr fun n => ?_
  rw [← mul_assoc, ← add_mul, mul_left_inj' I_ne_zero]
  norm_cast

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