re_eq_neg_norm

Mathlib.Analysis.Complex.Order

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

English

For all z ∈ ℂ, z.re = −||z|| if and only if z ≤ 0 in the complex order.

Русский

Для всех z ∈ ℂ, z.re = −||z|| тогда и только тогда, когда z ≤ 0 по комплексному порядку.

LaTeX

$$$z.re = -\|z\| \iff z \le 0$$$

Lean4

@[simp]
theorem re_eq_neg_norm {z : ℂ} : z.re = -‖z‖ ↔ z ≤ 0 := by rw [← neg_eq_iff_eq_neg, neg_re_eq_norm]

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

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

Разделы

Аффилиация

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