angle_smul_smul — Mathlib

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]

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