norm_exp_eq_iff_re_eq — Mathlib

English

For complex x,y, the equality of norms of exp x and exp y holds if and only if their real parts are equal.

Русский

Для комплексных чисел x,y равенство норм exp x и exp y выполняется тогда и только тогда, когда вещественная часть x равна вещественной части y.

LaTeX

$$$\\\\|\\\\exp x\\\\| = \\\\|\\\\exp y\\\\| \\\\iff x_{\\\\Re} = y_{\\\\Re}$$$

Lean4

theorem norm_exp_eq_iff_re_eq {x y : ℂ} : ‖exp x‖ = ‖exp y‖ ↔ x.re = y.re := by rw [norm_exp, norm_exp, Real.exp_eq_exp]

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