[isabelle] New AFP Article: Ptolemy's Theorem



Ptolemy's Theorem
Lukas Bulwahn

This entry provides an analytic proof to Ptolemy's Theorem using polar form transformation and trigonometric identities. In this formalization, we use ideas from John Harrison's HOL Light formalization and the proof sketch on the Wikipedia entry of Ptolemy's Theorem. This theorem is the 95th theorem of the Top 100 Theorems list.

https://www.isa-afp.org/entries/Ptolemys_Theorem.shtml

Only 29 theorems to go...

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.