Pascal's theorem in real projective plane

DOI10.1515/forma-2017-0011zbMath1377.51003OpenAlexW2758751785MaRDI QIDQ2407506

Roland Coghetto

Publication date: 6 October 2017

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1515/forma-2017-0011

zbMATH Keywords

real projective planePascal's theoremGrassman-Plücker relation

Mathematics Subject Classification ID

Finite affine and projective planes (geometric aspects) (51E15) Mechanization of proofs and logical operations (03B35) Projective analytic geometry (51N15)

Related Items (2)

Pappus's hexagon theorem in real projective plane ⋮ Klein-Beltrami model. II

Uses Software

• Mizar
• Prover9
• HOL Light
• OTT2MIZ

Cites Work

• Unnamed Item
• Mechanizing complemented lattices within Mizar type system
• Homography in \(\mathbb{R}\mathbb{P}^2\)
• ATP and presentation service for Mizar formalizations
• Group of homography in real projective plane
• Mizar: State-of-the-art and Beyond
• Types for Proofs and Programs

This page was built for publication: Pascal's theorem in real projective plane