exp_eq_exp_iff_exp_sub_eq_one

Mathlib.Analysis.SpecialFunctions.Complex.Log

URI: https://scilib.ai/kg/mathlib#Complex.exp_eq_exp_iff_exp_sub_eq_one

English

For complex numbers x and y, exp x = exp y if and only if exp(x − y) = 1.

Русский

Для комплексных чисел x и y верно: exp x = exp y тогда и только тогда, когда exp(x − y) = 1.

LaTeX

$$$\exp x = \exp y \iff \exp(x - y) = 1$$$

Lean4

theorem exp_eq_exp_iff_exp_sub_eq_one {x y : ℂ} : exp x = exp y ↔ exp (x - y) = 1 := by
  rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru