Homography in \(\mathbb{R}\mathbb{P}^2\)
type: Item
instance of: scholarly article
title: Homography in \(\mathbb{R}\mathbb{P}^2\)
zbMATH Open document ID: 1357.51021
author: Roland Coghetto
published in: Formalized Mathematics
publication date: 2017-04-03T00:00:00Z
Mathematics Subject Classification ID: 51N15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 6699641
zbMATH Keywords: projectivity
zbMATH Keywords: projective transformation
zbMATH Keywords: projective collineation
zbMATH Keywords: real projective plane
zbMATH Keywords: Grassmann-Plücker relation
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: Mizar
MaRDI profile type: Publication
full work available at URL: forma-2016-0020
OpenAlex ID: W2592432152
cites work: Cayley factorization and the area principle
cites work: Cancellation Patterns in Automatic Geometric Theorem Proving
cites work: Mizar: State-of-the-art and Beyond
cites work: A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry
cites work: Q3980491
cites work: Formalizing Projective Plane Geometry in Coq
cites work: Linear transformations of Euclidean topological spaces
cites work: Mechanical theorem proving in projective geometry
cites work: Perspectives on Projective Geometry
DOI: 10.1515/FORMA-2016-0020
description: scientific article; zbMATH DE number 6699641