English
Let x be a complex number. Then ||x|| = 1 if and only if there exists a real θ with -π < θ ≤ π such that x = exp(i θ).
Русский
Пусть x — комплексное число. Тогда ||x|| = 1 тогда и только тогда, когда существует вещественное θ такое, что -π < θ ≤ π и x = e^{iθ}.
LaTeX
$$$\\\\|x\\\\| = 1 \\\\iff \\\\exists \\\\theta \in (-\\\\pi, \\\\pi], \\\\exp(i \\\\theta) = x$$$
Lean4
theorem norm_eq_one_iff' : ‖x‖ = 1 ↔ ∃ θ ∈ Set.Ioc (-π) π, exp (θ * I) = x :=
by
rw [norm_eq_one_iff]
constructor
· rintro ⟨θ, rfl⟩
refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
· convert toIocMod_mem_Ioc _ _ _
ring
·
rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub, ofReal_zsmul, ofReal_mul, ofReal_ofNat,
exp_mul_I_periodic.sub_zsmul_eq]
· rintro ⟨θ, _, rfl⟩
exact ⟨θ, rfl⟩
