V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = ‖x‖ * ‖y‖
⊢ angle x y = 0
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ inner x y = ‖x‖ * ‖y‖ ↔ angle x y = 0
refine' ⟨fun h => _, inner_eq_mul_norm_of_angle_eq_zero⟩
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = ‖x‖ * ‖y‖
h₁ : ‖x‖ * ‖y‖ ≠ 0
⊢ angle x y = 0
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = ‖x‖ * ‖y‖
⊢ angle x y = 0
have h₁ : ‖x‖ * ‖y‖ ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne'
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = ‖x‖ * ‖y‖
h₁ : ‖x‖ * ‖y‖ ≠ 0
⊢ angle x y = 0
rw [angle, h, div_self h₁, Real.arccos_one]