Homography in RP^2

DOI10.1515/FORMA-2016-0020MaRDI QIDQ520382zbMATHOpenAlexFDO

Authors Roland Coghetto

Publication date 3 April 2017

Published in Formalized Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1515/forma-2016-0020

zbMATH Keywords

projectivityprojective transformationreal projective planeprojective collineationGrassmann-Plücker relation

Mathematics Subject Classification ID

Projective analytic geometry (51N15) Mechanization of proofs and logical operations (03B35)

Recommendations

• Group of homography in real projective plane
• Pappus's hexagon theorem in real projective plane
• Publication:4728920
• Duality notions in real projective plane
• Formalizing projective plane geometry in Coq

Cites work

• scientific article; zbMATH DE number 22547 (Why is no real title available?)
• A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
• Cancellation patterns in automatic geometric theorem proving
• Cayley factorization and the area principle
• Formalizing projective plane geometry in Coq
• Linear transformations of Euclidean topological spaces
• Mechanical theorem proving in projective geometry
• Mizar: state-of-the-art and beyond
• Perspectives on projective geometry. A guided tour through real and complex geometry

Cited in

(8)

• Pappus's hexagon theorem in real projective plane
• Factoring a homography to analyze projective distortion
• scientific article; zbMATH DE number 4063923 (Why is no real title available?)
• Group of homography in real projective plane
• Klein-Beltrami model. IV
• scientific article; zbMATH DE number 66909 (Why is no real title available?)
• Klein-Beltrami model. II
• Pascal's theorem in real projective plane

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• Mizar

This page was built for publication: Homography in \(\mathbb{R}\mathbb{P}^2\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q520382)