neg_re_eq_norm

Mathlib.Analysis.Complex.Order

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

← MathLib Explorer

English

For any 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 neg_re_eq_norm {z : ℂ} : -z.re = ‖z‖ ↔ z ≤ 0 :=
  by
  rw [← neg_re, ← norm_neg z, re_eq_norm]
  exact neg_nonneg.and <| eq_comm.trans neg_eq_zero

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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