V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ ‖x‖ * ‖y‖ = 0 → inner x y = 0
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ cos (angle x y) * (‖x‖ * ‖y‖) = inner x y
rw [cos_angle, div_mul_cancel_of_imp]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ ‖x‖ * ‖y‖ = 0 → inner x y = 0
simp (config := { contextual := true }) [or_imp]