| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Ptolemy's Theorem
| Title: | Ptolemy's Theorem |
| Author: | Lukas Bulwahn (lukas /dot/ bulwahn /at/ gmail /dot/ com) |
| Submission date: | 2016-08-07 |
| Abstract: | 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. |
| BibTeX: |
@article{Ptolemys_Theorem-AFP,
author = {Lukas Bulwahn},
title = {Ptolemy's Theorem},
journal = {Archive of Formal Proofs},
month = aug,
year = 2016,
note = {\url{http://isa-afp.org/entries/Ptolemys_Theorem.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [skipped] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|