V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ : V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
⊢ angle (c • x) (c • y) = angle x y
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ : V
c : ℝ
hc : c ≠ 0
x y : V
⊢ angle (c • x) (c • y) = angle x y
have : c * c ≠ 0 := mul_ne_zero hc hc
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ : V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
⊢ angle (c • x) (c • y) = angle x y
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]