Duality notions in real projective plane

DOI10.2478/forma-2021-0016zbMath1494.68295OpenAlexW4285325858MaRDI QIDQ2171520

Roland Coghetto

Publication date: 9 September 2022

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

Full work available at URL: https://doi.org/10.2478/forma-2021-0016

zbMATH Keywords

dualityreal projective planeconverse theoremprinciple of duality

Mathematics Subject Classification ID

General theory of linear incidence geometry and projective geometries (51A05) Projective analytic geometry (51N15) Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• Unnamed Item
• Unnamed Item
• A case study in formalizing projective geometry in Coq: Desargues theorem
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Klein-Beltrami model. I
• Formalizing constructive projective geometry in Agda
• Formalizing Projective Plane Geometry in Coq
• Mizar: State-of-the-art and Beyond
• The real projective spaces in homotopy type theory

This page was built for publication: Duality notions in real projective plane