Documentation

Mathlib.Analysis.Complex.Arg

Rays in the complex numbers #

This file links the definition SameRay ℝ x y with the equality of arguments of complex numbers, the usual way this is considered.

Main statements #

theorem Complex.sameRay_iff {x : } {y : } :
SameRay x y x = 0 y = 0 x.arg = y.arg
theorem Complex.sameRay_iff_arg_div_eq_zero {x : } {y : } :
SameRay x y (x / y).arg = 0
theorem Complex.abs_add_eq_iff {x : } {y : } :
Complex.abs (x + y) = Complex.abs x + Complex.abs y x = 0 y = 0 x.arg = y.arg
theorem Complex.abs_sub_eq_iff {x : } {y : } :
Complex.abs (x - y) = |Complex.abs x - Complex.abs y| x = 0 y = 0 x.arg = y.arg
theorem Complex.sameRay_of_arg_eq {x : } {y : } (h : x.arg = y.arg) :
theorem Complex.abs_add_eq {x : } {y : } (h : x.arg = y.arg) :
Complex.abs (x + y) = Complex.abs x + Complex.abs y
theorem Complex.abs_sub_eq {x : } {y : } (h : x.arg = y.arg) :
Complex.abs (x - y) = Complex.abs x - Complex.abs y