References
- [1] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.10.1007/978-3-319-20615-8_17
- [2] Roland Coghetto. Klein-Beltrami model. Part I. Formalized Mathematics, 26(1):21–32, 2018. doi:10.2478/forma-2018-0003.10.2478/forma-2018-0003
- [3] Roland Coghetto. Klein-Beltrami model. Part II. Formalized Mathematics, 26(1):33–48, 2018. doi:10.2478/forma-2018-0004.10.2478/forma-2018-0004
- [4] Noboru Endou. Complex linear space and complex normed space. Formalized Mathematics, 12(2):93–102, 2004.
- [5] Jadwiga Knop. About a certain generalization of the affine ratio of three points and unharmonic ratio of four points. Bulletin of the Section of Logic, 32(1–2):33–42, 2003.
- [6] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.
- [7] Kazuhisa Nakasho and Yasunari Shidama. Documentation generator focusing on symbols for the HTML-ized Mizar library. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, CICM 2015, volume 9150 of Lecture Notes in Computer Science, pages 343–347. Springer, Cham, 2015. doi:10.1007/978-3-319-20615-8_25.10.1007/978-3-319-20615-8_25
- [8] Athanase Papadopoulos and Sumio Yamada. On the projective geometry of constant curvature spaces. Sophus Lie and Felix Klein: The Erlangen Program and Its Impact in Mathematics and Physics, 23:237–245, 2015.
- [9] Jürgen Richter-Gebert. Perspectives on projective geometry: a guided tour through real and complex geometry. Springer Science & Business Media, 2011.
- [10] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990.