English
For nonzero x,y, the cosine of the oriented angle equals the inner product divided by the product of the norms: Real.Angle.cos(o.oangle x y) = ⟪x,y⟫ / (‖x‖ ‖y‖).
Русский
Для ненулевых векторов x,y косинус ориентированного угла равен отношению скалярного произведения к произведению норм: Real.Angle.cos(o.oangle x y) = ⟪x,y⟫ / (‖x‖ ‖y‖).
LaTeX
$$$ x \neq 0 \land y \neq 0 \Rightarrow Real.Angle.cos(o.oangle x y) = \langle x,y \rangle /( \|x\| \cdot \|y\|) $$$
Lean4
/-- The inner product of two vectors is the product of the norms and the cosine of the oriented
angle between the vectors. -/
theorem inner_eq_norm_mul_norm_mul_cos_oangle (x y : V) : ⟪x, y⟫ = ‖x‖ * ‖y‖ * Real.Angle.cos (o.oangle x y) :=
by
by_cases hx : x = 0; · simp [hx]
by_cases hy : y = 0; · simp [hy]
rw [oangle, Real.Angle.cos_coe, Complex.cos_arg, o.norm_kahler]
· simp only [kahler_apply_apply, real_smul, add_re, ofReal_re, mul_re, I_re, ofReal_im]
simp [field]
· exact o.kahler_ne_zero hx hy
