angle_mul_left — Mathlib

English

If a ≠ 0, then the angle between a x and a y equals the angle between x and y, for any x,y.

Русский

Если a ≠ 0, то угол между a x и a y равен углу между x и y, для любых x,y.

LaTeX

$$$$\angle(a x, a y) = \angle(x,y) \quad (a \ne 0).$$$$

Lean4

@[simp]
theorem angle_mul_left (ha : a ≠ 0) (x y : ℂ) : angle (a * x) (a * y) = angle x y := by
  obtain rfl | hx := eq_or_ne x 0 <;> obtain rfl | hy := eq_or_ne y 0 <;> simp [angle_eq_abs_arg, mul_div_mul_left, *]

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