The level of real projective spaces.
Stephan Stolz (1989)
Commentarii mathematici Helvetici
Similarity:
Stephan Stolz (1989)
Commentarii mathematici Helvetici
Similarity:
Ted Petrie (1976)
Commentarii mathematici Helvetici
Similarity:
Paul Lévy (1943/44)
Commentarii mathematici Helvetici
Similarity:
Michael N. Dyer (1976)
Commentarii mathematici Helvetici
Similarity:
R. Sridharan, M. Ojanguren (1969)
Commentarii mathematici Helvetici
Similarity:
Micheal Dyer (1984)
Commentarii mathematici Helvetici
Similarity:
Louis Kollros (1943/44)
Commentarii mathematici Helvetici
Similarity:
P. de de Harpe (1979)
Commentarii mathematici Helvetici
Similarity:
Andrew J. Sommese, M. Andreatta (1991)
Commentarii mathematici Helvetici
Similarity:
Boskoff, Wladimir G., Suceavă, Bogdan D. (2008)
Beiträge zur Algebra und Geometrie
Similarity:
Roland Coghetto (2016)
Formalized Mathematics
Similarity:
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]. Some definitions on the real projective spaces were introduced early in the Mizar Mathematical Library by Wojciech Leonczuk [9], Krzysztof Prazmowski [10] and by Wojciech Skaba [18]. In this article, we check with the Mizar system [4], some properties on the determinants and the Grassmann-Plücker relation in rank 3 [2], [1], [7],...