angle_div_left_eq_angle_mul_right

English

For any nonzero a, the angle between x/a and y equals the angle between x and y a.

Русский

Для любого ненулевого a угол между x/a и y равен углу между x и y a.

LaTeX

$$$$\angle\left(\frac{x}{a}, y\right) = \angle\left(x, y a\right).$$$$

Lean4

theorem angle_div_left_eq_angle_mul_right (a x y : ℂ) : angle (x / a) y = angle x (y * a) :=
  by
  obtain rfl | ha := eq_or_ne a 0
  · simp
  · rw [← angle_mul_right ha, div_mul_cancel₀ _ ha]

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