Group of Homography in Real Projective Plane

Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group.

Bibliographic Details
Main Author:	Coghetto Roland
Format:	Article
Language:	English
Published:	Sciendo 2017-03-01
Series:	Formalized Mathematics
Subjects:	51n15 03b35 projectivity projective transformation real projective plane group of homography identifier: anproj_9 version: 8.1.05 5.40.1289
Online Access:	https://doi.org/10.1515/forma-2017-0005

id	doaj-e87e00da32bf4f6da7d6bb0e11a41404
record_format	Article
spelling	doaj-e87e00da32bf4f6da7d6bb0e11a414042021-09-05T20:45:04ZengSciendoFormalized Mathematics1898-99342017-03-01251556210.1515/forma-2017-0005forma-2017-0005Group of Homography in Real Projective PlaneCoghetto Roland0Rue de la Brasserie 5, 7100, La Louvière, BelgiumUsing the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group.https://doi.org/10.1515/forma-2017-000551n1503b35projectivityprojective transformationreal projective planegroup of homographyidentifier: anproj_9version: 8.1.05 5.40.1289
collection	DOAJ
language	English
format	Article
sources	DOAJ
author	Coghetto Roland
spellingShingle	Coghetto Roland Group of Homography in Real Projective Plane Formalized Mathematics 51n15 03b35 projectivity projective transformation real projective plane group of homography identifier: anproj_9 version: 8.1.05 5.40.1289
author_facet	Coghetto Roland
author_sort	Coghetto Roland
title	Group of Homography in Real Projective Plane
title_short	Group of Homography in Real Projective Plane
title_full	Group of Homography in Real Projective Plane
title_fullStr	Group of Homography in Real Projective Plane
title_full_unstemmed	Group of Homography in Real Projective Plane
title_sort	group of homography in real projective plane
publisher	Sciendo
series	Formalized Mathematics
issn	1898-9934
publishDate	2017-03-01
description	Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group.
topic	51n15 03b35 projectivity projective transformation real projective plane group of homography identifier: anproj_9 version: 8.1.05 5.40.1289
url	https://doi.org/10.1515/forma-2017-0005
work_keys_str_mv	AT coghettoroland groupofhomographyinrealprojectiveplane
_version_	1717784586687086592

Group of Homography in Real Projective Plane

Similar Items