norm_eq_one_iff — Mathlib

English

For any complex z, |z| = 1 if and only if z = e^{iθ} for some θ ∈ ℝ.

Русский

Для любого z ∈ ℂ, |z| = 1 тогда и только тогда, когда z = e^{iθ} для некоторого θ ∈ ℝ.

LaTeX

$$$\\|z\\| = 1 \\iff \\exists \\theta \\\\in \\\\mathbb{R}, e^{i\\\\theta} = z$$$

Lean4

theorem norm_eq_one_iff (z : ℂ) : ‖z‖ = 1 ↔ ∃ θ : ℝ, exp (θ * I) = z :=
  by
  refine ⟨fun hz => ⟨arg z, ?_⟩, ?_⟩
  ·
    calc
      exp (arg z * I) = ‖z‖ * exp (arg z * I) := by rw [hz, ofReal_one, one_mul]
      _ = z := norm_mul_exp_arg_mul_I z
  · rintro ⟨θ, rfl⟩
    exact Complex.norm_exp_ofReal_mul_I θ

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