Homography in \(\mathbb{R}\mathbb{P}^2\)

DOI10.1515/forma-2016-0020zbMath1357.51021OpenAlexW2592432152MaRDI QIDQ520382

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 planeGrassmann-Plücker relationprojective collineation

Mathematics Subject Classification ID

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

Related Items (4)

Klein-Beltrami model. IV ⋮ Pascal's theorem in real projective plane ⋮ Klein-Beltrami model. II ⋮ Group of homography in real projective plane

Uses Software

• Coq
• Isabelle/HOL
• Mizar

Cites Work

• Unnamed Item
• Mechanical theorem proving in projective geometry
• Linear Transformations of Euclidean Topological Spaces
• Formalizing Projective Plane Geometry in Coq
• Perspectives on Projective Geometry
• Cancellation Patterns in Automatic Geometric Theorem Proving
• A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry
• Mizar: State-of-the-art and Beyond
• Cayley factorization and the area principle

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