ext_norm_arg — Mathlib

English

Two complex numbers are equal if they have the same modulus and the same argument: x = y iff |x| = |y| and arg x = arg y.

Русский

Два комплексных числа равны тогда и только тогда, когда у них одинаковый модуль и одинаковый аргумент: x = y ⇔ |x| = |y| и arg x = arg y.

LaTeX

$$$x = y \\iff \\|x\\| = \\|y\\| \\wedge \\arg x = \\arg y$$$

Lean4

theorem ext_norm_arg {x y : ℂ} (h₁ : ‖x‖ = ‖y‖) (h₂ : x.arg = y.arg) : x = y := by
  rw [← norm_mul_exp_arg_mul_I x, ← norm_mul_exp_arg_mul_I y, h₁, h₂]

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