ext_norm_arg_iff — Mathlib

English

Two complex numbers are equal if and only if their moduli are equal and their arguments are equal.

Русский

Два комплексных числа равны тогда и только тогда, когда равны их модули и аргументы.

LaTeX

$$forall {x y : ℂ}, x = y ↔ ∥x∥ = ∥y∥ ∧ arg x = arg y$$

Lean4

theorem ext_norm_arg_iff {x y : ℂ} : x = y ↔ ‖x‖ = ‖y‖ ∧ arg x = arg y :=
  ⟨fun h => h ▸ ⟨rfl, rfl⟩, and_imp.2 ext_norm_arg⟩

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