The real projective plane has been formalized in Isabelle/HOL by Timothy Makarios [
Some definitions on the real projective spaces were introduced early in the Mizar Mathematical Library by Wojciech Leonczuk [
In this article, we check with the Mizar system [
Then we show that the projective space induced (in the sense defined in [
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.