Email Gateway (Aug 22 2022 at 13:56): Email Gateway (Aug 22 2022 at 13:56):From: Tobias Nipkow <nipkow@in.tum.de>
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...
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC