Homography in ℝℙ

The real projective plane has been formalized in Isabelle/HOL by Timothy Makarios [13] and in Coq by Nicolas Magaud, Julien Narboux and Pascal Schreck [12].

Bibliographic Details
Main Author: Coghetto Roland
Format: Article
Language:English
Published: Sciendo 2016-12-01
Series:Formalized Mathematics
Subjects:
Online Access:https://doi.org/10.1515/forma-2016-0020
Description
Summary:The real projective plane has been formalized in Isabelle/HOL by Timothy Makarios [13] and in Coq by Nicolas Magaud, Julien Narboux and Pascal Schreck [12].
ISSN:1426-2630
1898-9934