sameRay_iff_arg_div_eq_zero — Mathlib

English

If x.arg = y.arg then x and y lie on the same ray.

Русский

Если x.arg = y.arg, то x и y лежат на одной луче.

LaTeX

$$$$\text{SameRay}_{\mathbb{R}}(x,y) \quad \text{if } x.\arg = y.\arg.$$$$

Lean4

theorem sameRay_iff_arg_div_eq_zero : SameRay ℝ x y ↔ arg (x / y) = 0 :=
  by
  rw [← Real.Angle.toReal_zero, ← arg_coe_angle_eq_iff_eq_toReal, sameRay_iff]
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0; · simp [hy]
  simp [hx, hy, arg_div_coe_angle, sub_eq_zero]

Похожие утверждения