inner_eq_neg_mul_norm_of_angle_eq_pi

English

If the angle between x and y is π, then their inner product equals the negative product of their norms.

Русский

Если угол между x и y равен π, то их скалярное произведение равно отрицательному произведению их норм.

LaTeX

$$$\\\\langle x, y\\\\rangle = -(\\\\|x\\\\| \\\\cdot \\\\|y\\\\|)$ при $\\\\angle x y = \\\\pi$$$

Lean4

/-- If the angle between two vectors is π, the inner product equals the negative product
of the norms. -/
theorem inner_eq_neg_mul_norm_of_angle_eq_pi {x y : V} (h : angle x y = π) : ⟪x, y⟫ = -(‖x‖ * ‖y‖) := by
  simp [← cos_angle_mul_norm_mul_norm, h]

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