sameRay_iff — Mathlib

English

Two nonzero complex numbers x,y are on the same ray (over ℝ) if and only if arg(x/y) = 0.

Русский

Два ненулевых комплексных числа x и y лежат на одной луче над ℝ тогда и только тогда, когда arg(x/y) = 0.

LaTeX

$$$$\text{SameRay}_{\mathbb{R}}(x,y) \iff \arg\left(\frac{x}{y}\right) = 0.$$$$

Lean4

theorem sameRay_iff : SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg :=
  by
  rcases eq_or_ne x 0 with (rfl | hx)
  · simp
  rcases eq_or_ne y 0 with (rfl | hy)
  · simp
  simp only [hx, hy, sameRay_iff_norm_smul_eq, arg_eq_arg_iff hx hy]
  simp [field, hx]
  rw [mul_comm, eq_comm]

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