mathlib3 documentation

geometry.euclidean.sphere.ptolemy

Ptolemy's theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves Ptolemy's theorem on the lengths of the diagonals and sides of a cyclic quadrilateral.

Main theorems #

TODO: The current statement of Ptolemy’s theorem works around the lack of a "cyclic polygon" concept in mathlib, which is what the theorem statement would naturally use (or two such concepts, since both a strict version, where all vertices must be distinct, and a weak version, where consecutive vertices may be equal, would be useful; Ptolemy's theorem should then use the weak one).

An API needs to be built around that concept, which would include: