Pascal’s Theorem in Real Projective Plane

Article English OPEN
Coghetto Roland (2017)
  • Publisher: Sciendo
  • Journal: Formalized Mathematics (issn: 1426-2630, eissn: 1898-9934)
  • Related identifiers: doi: 10.1515/forma-2017-0011
  • Subject: 51N15 | Mathematics | Grassman-Plücker relation | real projective plane | Pascal’s theorem | 03B35 | QA1-939 | 51E15
    arxiv: Mathematics::History and Overview

In this article we check, with the Mizar system [2], Pascal’s theorem in the real projective plane (in projective geometry Pascal’s theorem is also known as the Hexagrammum Mysticum Theorem)1. Pappus’ theorem is a special case of a degenerate conic of two lines.
Share - Bookmark