English
For nonzero complex numbers x and y, the angle between x and y equals the absolute value of the argument of their quotient.
Русский
Для ненулевых комплексных чисел x и y угол между ними равен модулю аргументаQuotient x/y.
LaTeX
$$$$\angle(x,y) = \bigl| \arg\left( \frac{x}{y} \right) \bigr| \quad (x \ne 0,\ y \ne 0).$$$$
Lean4
/-- The angle between two non-zero complex numbers is the absolute value of the argument of their
quotient.
Note that this does not hold when `x` or `y` is `0` as the LHS is `π / 2` while the RHS is `0`. -/
theorem angle_eq_abs_arg (hx : x ≠ 0) (hy : y ≠ 0) : angle x y = |(x / y).arg| :=
by
refine Real.arccos_eq_of_eq_cos (abs_nonneg _) (abs_arg_le_pi _) ?_
rw [Real.cos_abs, Complex.cos_arg (div_ne_zero hx hy)]
simp [div_eq_mul_inv, Complex.normSq_eq_norm_sq]
field_simp
