English
The law of cosines holds for triangles in Euclidean space in angle form with side lengths expressed by distances.
Русский
Закон косинусов применяется к треуголникам в евклидовом пространстве через длины сторон.
LaTeX
$$$\operatorname{dist}(p_1,p_3)^2 = \operatorname{dist}(p_1,p_2)^2 + \operatorname{dist}(p_3,p_2)^2 - 2\operatorname{dist}(p_1,p_2)\operatorname{dist}(p_3,p_2}\cos(\angle p_1 p_2 p_3)$$$
Lean4
/-- **Law of cosines** (cosine rule), angle-at-point form. -/
theorem dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle (p₁ p₂ p₃ : P) :
dist p₁ p₃ * dist p₁ p₃ =
dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ - 2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (∠ p₁ p₂ p₃) :=
by
rw [dist_eq_norm_vsub V p₁ p₃, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₃ p₂]
unfold angle
convert norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle (p₁ -ᵥ p₂ : V) (p₃ -ᵥ p₂ : V)
· exact (vsub_sub_vsub_cancel_right p₁ p₃ p₂).symm
· exact (vsub_sub_vsub_cancel_right p₁ p₃ p₂).symm
