English
For any nonzero real c and vectors x, y, the angle between c x and c y equals the angle between x and y.
Русский
Для любого ненулевого действительного числа c и векторов x, y угол между c x и c y равен углу между x и y.
LaTeX
$$$$ \angle (c\,x) (c\,y) = \angle x y \quad (c \neq 0). $$$$
Lean4
theorem angle_smul_smul {c : ℝ} (hc : c ≠ 0) (x y : V) : angle (c • x) (c • y) = angle x y :=
by
have : c * c ≠ 0 := mul_ne_zero hc hc
rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]