Public Mathlib landmark · existing upstream theorem · read-only
ProofAtlas

Geometry · existing Mathlib declaration

Law of Cosines

Choose any three points and focus on the angle at p₂. The distance from p₁ to p₃ satisfies the familiar cosine rule using the two distances from p₂—even when the three points form a degenerate triangle.

The theorem at a glance

Law of Cosines at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

For any three points in a real inner-product affine space, the squared distance p₁—p₃ obeys the cosine rule for the angle at p₂. Generated explanation only; the exact HTML statement and pinned source are authoritative.
Detailed visual description

The poster fixes the angle and opposite side in one labelled triangle, prints the source's distance-product identity, and follows the checked proof from distances to displacement norms, through the vector law of cosines, to cancellation of the shared affine base point. Its exact-scope footer keeps degenerate triples inside the declaration.

Formal orientation

Statement map

Statement map for Law of CosinesFor any three points in a real inner-product affine space, the squared distance opposite the angle at p₂ is determined by the two adjacent distances and the cosine of that angle. The pinned upstream declaration is EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle. The exact checked statement is theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (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₃).Mathematical readingFor any three points ina real inner-productaffine space, thesquared distanceopposite the angle at p₂is determined by the twoadjacent distances andthe cosine of thatangle.Pinned declarationmathlib ·EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angleExact checked formtheoremEuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle{V : Type*} {P : Type*}[NormedAddCommGroup V][InnerProductSpace ℝ V][MetricSpace P][NormedAddTorsor V P](p₁ p₂ p₃ : P) : dist p₁p₃ * dist p₁ p₃ = distp₁ p₂ * dist p₁ p₂ +dist p₃ p₂ * dist p₃ p₂- 2 * dist p₁ p₂ * distp₃ p₂ * Real.cos (∠ p₁p₂ p₃)Statement map for Law of CosinesFor any three points in a real inner-product affine space, the squared distance opposite the angle at p₂ is determined by the two adjacent distances and the cosine of that angle. The pinned upstream declaration is EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle. The exact checked statement is theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (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₃).Mathematical readingFor any three points ina real inner-productaffine space, thesquared distanceopposite the angle at p₂is determined by the twoadjacent distances andthe cosine of thatangle.Pinned declarationmathlib ·EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angleExact checked formtheoremEuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle{V : Type*} {P : Type*}[NormedAddCommGroup V][InnerProductSpace ℝ V][MetricSpace P][NormedAddTorsor V P](p₁ p₂ p₃ : P) : dist p₁p₃ * dist p₁ p₃ = distp₁ p₂ * dist p₁ p₂ +dist p₃ p₂ * dist p₃ p₂- 2 * dist p₁ p₂ * distp₃ p₂ * Real.cos (∠ p₁p₂ p₃)

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

For the angle at p₂, the law of cosines relates the opposite distance p₁—p₃ to the two distances from p₂. Scientific diagram · explanatory, not proof evidence.
Detailed visual description

This page indexes Mathlib's angle-at-point law of cosines for arbitrary points p₁, p₂, and p₃ in an affine metric space modeled on a real inner-product space. The selected identity places the angle at p₂ and the opposite distance between p₁ and p₃. It assumes neither distinctness nor non-collinearity, so degenerate triples are included. It is not restricted to the Euclidean plane and does not state the law of sines, recover an angle, or add a nondegenerate-triangle hypothesis.

Complementary intuition

A mathematical landmark

The law of cosines is the basic metric identity connecting three side lengths with one angle. Mathlib states it without unnecessary nondegeneracy or planar hypotheses and derives it cleanly from the vector law of cosines through affine displacement vectors.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (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₃)
Selected evidence declaration text
theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (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₃)

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally
Locally reproducedExact upstream declaration replayed
Reviewed pageCurrent public presentation reviewed
Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Claim boundary

No new theorem is claimed

This page indexes Mathlib's angle-at-point law of cosines for arbitrary points p₁, p₂, and p₃ in an affine metric space modeled on a real inner-product space. The selected identity places the angle at p₂ and the opposite distance between p₁ and p₃. It assumes neither distinctness nor non-collinearity, so degenerate triples are included. It is not restricted to the Euclidean plane and does not state the law of sines, recover an angle, or add a nondegenerate-triangle hypothesis.

Provenance

Origin and evidence stay separate

Existing declaration
EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle in mathlib
Relationship
The checked artifact is the upstream declaration itself
Preferred checked artifact
artifact.library.mathlib.law-of-cosines.v001
Source handling
Verified upstream reference; no mirrored source package