Klein-Beltrami model. III

DOI10.2478/forma-2020-0001zbMath1462.68222OpenAlexW4211215417MaRDI QIDQ2658806

Roland Coghetto

Publication date: 24 March 2021

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

Full work available at URL: https://doi.org/10.2478/forma-2020-0001

zbMATH Keywords

foundations of geometryTarski's geometry axiomsKlein-Beltrami model

Mathematics Subject Classification ID

Hyperbolic and elliptic geometries (general) and generalizations (51M10) General theory of linear incidence geometry and projective geometries (51A05) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Isabelle/HOL
• Mizar

Cites Work

• Tarski geometry axioms. II
• Klein-Beltrami model. II
• Group of homography in real projective plane
• Mizar: State-of-the-art and Beyond
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Klein-Beltrami model. III