mathlib3 documentation


Rays in the complex numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main statements #

theorem complex.same_ray_iff {x y : } :
same_ray x y x = 0 y = 0 x.arg = y.arg
theorem complex.same_ray_of_arg_eq {x y : } (h : x.arg = y.arg) :