English
The sine of the angle between x and y times the product of their norms equals the square root of the Gram determinant.
Русский
Синус угла между x и y, умноженный на произведение их норм, равен корню из детерминанта Грамма: sqrt(⟪x,x⟫⟪y,y⟫ - ⟪x,y⟫^2).
LaTeX
$$$\\\\sin(\\\\angle x y) \\\\cdot (\\\\|x\\\\| \\\\cdot \\\\|y\\\\|) = \\\\sqrt{\\\\⟪x, x\\\\⟫ \\\\cdot \\\\⟪y, y\\\\⟫ - \\\\⟪x, y\\\\⟫^2}$$$
Lean4
/-- The sine of the angle between two vectors, multiplied by the
product of their norms. -/
theorem sin_angle_mul_norm_mul_norm (x y : V) :
Real.sin (angle x y) * (‖x‖ * ‖y‖) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) :=
by
unfold angle
rw [Real.sin_arccos]
nth_rw 2 [← Real.sqrt_sq (mul_nonneg (norm_nonneg x) (norm_nonneg y))]
rw [← Real.sqrt_mul' _ (by positivity), sq]
rcases eq_or_ne x 0 with (rfl | hx); · simp
rcases eq_or_ne y 0 with (rfl | hy); · simp
simp only [real_inner_self_eq_norm_mul_norm]
field_simp
