LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Complex.Arg


Complex.sameRay_iff

theorem Complex.sameRay_iff : ∀ {x y : ℂ}, SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

This theorem states that for any two complex numbers `x` and `y`, they are in the same ray according to the `SameRay` definition if and only if either `x` is zero, `y` is zero, or the arguments of `x` and `y` (as defined by the `Complex.arg` function) are equal. In other words, two complex numbers are in the same ray if they are zero or they have the same argument (angle from the positive real axis in the complex plane).

More concisely: Complex numbers `x` and `y` lie on the same ray if and only if `x = 0`, `y = 0`, or `Complex.arg x = Complex.arg y`.