@ARTICLE{ANPROJ_8.MIZ,
    TITLE = {Homography in $\mathbb{RP}^2$},
    AUTHOR = {Coghetto, Roland},
    ADDRESS1 = {Rue de la Brasserie 5\\7100 La Louvi\`ere, Belgium},
    DAY = {18},
    MONTH = {October},
    YEAR = {2016},
    SUMMARY = {The real projective plane has been formalized in Isabelle/HOL
  by Timothy Makarios \cite{makarios2012mechanical} and
  in Coq by Nicols Magaud, Julien Narboux and
  Pascal Schreck \cite{magaud2008formalizing}. \par
  Some definitions on the real projective spaces were
  introduced early in the Mizar Mathematical Library (MML)
  by Wojciech Leonczuk and
  Krzysztof Prazmowski \cite{ANPROJ_1.ABS,ANPROJ_2.ABS} and
  by Wojciech Skaba \cite{COLLSP.ABS}.
  \par
  In this article, we check with the Mizar system \cite{Mizar-State-2015},
  some properties on the determinants and
  the Grassman-Pl\{¨}ucker relation in rank 3
  \cite{apel2010cancellation,apel2014geometry,fuchs2010formalization,
       richter1995mechanical,richter2011perspectives}.
  \par
  Then we show that the projective space induced
  (in the sense defined in \cite{ANPROJ_1.ABS})
  by $\mathbb{R}^3$ is a projective plane
  (in the sense defined in \cite{ANPROJ_2.ABS}).
  \par
  Finally, in the real projective plane, we define the homography
  induced by a 3-by-3 invertible matrix and we show that
  the images of 3 collinear points are themselves collinear.},
  MSC2010 = {51E45,51N15,03B35},
  KEYWORDS = {projectivity, projective transformation,
  projective collineation, real projective plane,
  Grassman-Pl{¨}ucker relation}}
  }

@incollection{apel2010cancellation,
  title={Cancellation patterns in automatic geometric theorem proving},
  author={Apel, Susanne and Richter-Gebert, J{\"u}rgen},
  booktitle={Automated Deduction in Geometry},
  pages={1--33},
  year={2010},
  publisher={Springer}
}
@phdthesis{apel2014geometry,
  title={The geometry of brackets and the area principle},
  author={Apel, Susanne and others}
}
@book{richter2011perspectives,
  title={Perspectives on projective geometry: a guided tour through real and complex geometry},
  author={Richter-Gebert, J{\"u}rgen},
  year={2011},
  publisher={Springer Science \& Business Media}
}
@article{richter1995mechanical,
  title={Mechanical theorem proving in projective geometry},
  author={Richter-Gebert, J{\"u}rgen},
  journal={Annals of Mathematics and Artificial Intelligence},
  volume={13},
  number={1-2},
  pages={139--172},
  year={1995},
  publisher={Springer}
}
@incollection{magaud2008formalizing,
  title={Formalizing projective plane geometry in Coq},
  author={Magaud, Nicolas and Narboux, Julien and Schreck, Pascal},
  booktitle={Automated Deduction in Geometry},
  pages={141--162},
  year={2008},
  publisher={Springer}
}
@incollection{fuchs2010formalization,
  title={A formalization of grassmann-cayley algebra in COQ and its application to theorem proving in projective geometry},
  author={Fuchs, Laurent and Thery, Laurent},
  booktitle={Automated Deduction in Geometry},
  pages={51--67},
  year={2010},
  publisher={Springer}
}
@book{makarios2012mechanical,
  title={A Mechanical Verification of the Independence of Tarski's Euclidean Axiom: A Thesis Submitted to the Victoria University of Wellington in Fulfilment of the Requirements for the Degree of Master of Science in Mathematics},
  author={Makarios, T.J.M.K.},
  url={https://books.google.be/books?id=76J2MwEACAAJ},
  year={2012},
  publisher={Victoria University of Wellington}
}

