im_le_neg_norm_iff_eq_neg_I_mul_norm

English

Let z be a complex-like element. Then Im(z) ≤ −|z| if and only if z is a purely imaginary negative multiple of its modulus, i.e. z = −i|z|.

Русский

Пусть z — некое комплексоподобное число. Тогда Im(z) ≤ −|z| эквивалентно тому, что z является отрицательным чисто мнимым кратным по модулю, то есть z = −i|z|.

LaTeX

$$$\\operatorname{Im}(z) \\le -\\|z\\| \\iff z = -\,i\\|z\\|$$$

Lean4

theorem im_le_neg_norm_iff_eq_neg_I_mul_norm {z : K} : im z ≤ -‖z‖ ↔ z = -(I * ‖z‖) := by
  simpa [neg_eq_iff_eq_neg, le_neg] using norm_le_im_iff_eq_I_mul_norm (z := -z)

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