cos_oangle_eq_inner_div_norm_mul_norm

English

Same as Cos Oangle with nonzero vectors: Real.Angle.cos(o.oangle x y) = ⟪x,y⟫/(‖x‖‖y‖) for x,y ≠ 0.

Русский

То же самое, что и Cos Oangle: Real.Angle.cos(o.oangle x y) = ⟪x,y⟫/(‖x‖‖y‖) при x ≠ 0, y ≠ 0.

LaTeX

$$$ x \neq 0 \land y \neq 0 \Rightarrow Real.Angle.cos(o.oangle x y) = ⟪x,y⟫/(\|x\| \|y\|) $$$

Lean4

/-- The cosine of the oriented angle between two nonzero vectors is the inner product divided by
the product of the norms. -/
theorem cos_oangle_eq_inner_div_norm_mul_norm {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    Real.Angle.cos (o.oangle x y) = ⟪x, y⟫ / (‖x‖ * ‖y‖) :=
  by
  rw [o.inner_eq_norm_mul_norm_mul_cos_oangle]
  field_simp

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