English
For any nonzero complex number z, the cosine of its argument equals the real part divided by the modulus: cos(arg z) = Re(z)/|z|.
Русский
Для любого ненулевого комплексного числа z косинус аргумента z равен действительной части z, делённой на модуль z: cos(arg z) = Re(z)/|z|.
LaTeX
$$$\\\\cos(\\\\arg z) = \\\\frac{\\\\Re(z)}{\\\\|z\\\\|}$$$
Lean4
theorem cos_arg {x : ℂ} (hx : x ≠ 0) : Real.cos (arg x) = x.re / ‖x‖ :=
by
rw [arg]
split_ifs with h₁ h₂
· rw [Real.cos_arcsin]
field_simp
simp [Real.sqrt_sq, (norm_pos_iff.mpr hx).le, *]
field_simp
· rw [Real.cos_add_pi, Real.cos_arcsin]
field_simp
simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]
field_simp
· rw [Real.cos_sub_pi, Real.cos_arcsin]
field_simp
simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]
field_simp
