Mathlib theorem · Existing formal mathematics
ProofAtlas

Existing in Mathlib · Geometry

Law of Sines

Mark the angles at p₂ and p₁ in a triangle. The sine at p₂ multiplied by the side p₂—p₃ equals the sine at p₁ multiplied by the side p₃—p₁. Mathlib keeps this as a division-free product identity, so the declaration also covers degenerate triples where a ratio form would need nonzero-side hypotheses.

Exact theorem

Exact Mathlib statement

theorem EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁

The theorem at a glance

Law of Sines at a glance

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

For any three points in a real inner-product affine space, Mathlib records the law of sines as a cross-multiplied identity that remains valid for degenerate triples. Explanatory diagram.
Detailed visual description

The poster marks the angles at p₂ and p₁ and their opposite sides, prints the exact two-term sine-distance equality, and follows the checked source from affine angles and distances through vector norms and the vector sine identity to the supplementary-angle sine step. Its exact-scope footer excludes any automatic ratio or nondegeneracy claim.

Statement structure

From hypotheses to conclusion

Statement map for Law of SinesFor any three points in a real inner-product affine space, the sine of the angle at p₂ times the distance p₂—p₃ equals the sine of the angle at p₁ times the distance p₃—p₁. The pinned upstream declaration is EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist. The exact checked statement is theorem EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁.Mathematical readingFor any three points ina real inner-productaffine space, the sineof the angle at p₂ timesthe distance p₂—p₃equals the sine of theangle at p₁ times thedistance p₃—p₁.Pinned declarationmathlib ·EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_distExact checked formtheoremEuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist{V : Type*} {P : Type*}[NormedAddCommGroup V][InnerProductSpace ℝ V][MetricSpace P][NormedAddTorsor V P](p₁ p₂ p₃ : P) :Real.sin (∠ p₁ p₂ p₃) *dist p₂ p₃ = Real.sin (∠p₃ p₁ p₂) * dist p₃ p₁Statement map for Law of SinesFor any three points in a real inner-product affine space, the sine of the angle at p₂ times the distance p₂—p₃ equals the sine of the angle at p₁ times the distance p₃—p₁. The pinned upstream declaration is EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist. The exact checked statement is theorem EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁.Mathematical readingFor any three points ina real inner-productaffine space, the sineof the angle at p₂ timesthe distance p₂—p₃equals the sine of theangle at p₁ times thedistance p₃—p₁.Pinned declarationmathlib ·EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_distExact checked formtheoremEuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist{V : Type*} {P : Type*}[NormedAddCommGroup V][InnerProductSpace ℝ V][MetricSpace P][NormedAddTorsor V P](p₁ p₂ p₃ : P) :Real.sin (∠ p₁ p₂ p₃) *dist p₂ p₃ = Real.sin (∠p₃ p₁ p₂) * dist p₃ p₁

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

The product form pairs the angle at p₂ with side p₂—p₃ and the angle at p₁ with side p₃—p₁ through the displayed opposite angle-side correspondences. Explanatory scientific diagram.
Detailed visual description

Exactly three labeled point markers form an oblique scalene triangle with no right angle. Exactly two double-stroked angle markings appear. The gold marking at p₁ is paired by color and double line with its opposite side p₂—p₃, and the cobalt marking at p₂ is paired by color and dashed line with its opposite side p₃—p₁. Each marking has two nested curved strokes; there is no angle marking at p₃ and no third side pairing. Below, the gold double line and cobalt dashed line cross at one neutral open ring, evoking the cross-multiplied product relation without printing a ratio, equality sign, distance, or sine formula.

Why it matters

A mathematical landmark

The law of sines is a fundamental bridge between angles and side lengths. Mathlib's selected declaration records its robust cross-multiplied form in any real inner-product affine space, and its proof connects the affine triangle to a vector sine-norm identity without adding planar or nondegeneracy assumptions.

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

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

This page indexes Mathlib's division-free angle-at-point law of sines for arbitrary points p₁, p₂, and p₃ in an affine metric space modeled on a real inner-product space. The selected endpoint is exactly Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁. It assumes neither distinctness nor non-collinearity and is not limited to the Euclidean plane. It does not itself state a quotient identity, justify division by either distance, or present all three cyclic ratios in one declaration.

Source and local evidence

Where the theorem comes from

Existing declaration
EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist in mathlib
Relationship
The checked artifact is the upstream declaration itself
Local Lean evidence
artifact.library.mathlib.law-of-sines.v001
Source
Open the pinned upstream reference