### On a dependence between polarities and an order of a projective plane

Jaroslava Jachanová, Helena Žáková (1976)

Sborník prací Přírodovědecké fakulty University Palackého v Olomouci. Matematika

Similarity:

Skip to main content (access key 's'),
Skip to navigation (access key 'n'),
Accessibility information (access key '0')

Jaroslava Jachanová, Helena Žáková (1976)

Sborník prací Přírodovědecké fakulty University Palackého v Olomouci. Matematika

Similarity:

Marek Jukl (1997)

Acta Universitatis Palackianae Olomucensis. Facultas Rerum Naturalium. Mathematica

Similarity:

Pfeiffer, Thorsten (1998)

Beiträge zur Algebra und Geometrie

Similarity:

Roland Coghetto (2017)

Formalized Mathematics

Similarity:

In this article we check, with the Mizar system [2], Pascal’s theorem in the real projective plane (in projective geometry Pascal’s theorem is also known as the Hexagrammum Mysticum Theorem)1. Pappus’ theorem is a special case of a degenerate conic of two lines. For proving Pascal’s theorem, we use the techniques developed in the section “Projective Proofs of Pappus’ Theorem” in the chapter “Pappus’ Theorem: Nine proofs and three variations” [11]. We also follow some ideas from Harrison’s...

Oswald Gschnitzer (1996)

Manuscripta mathematica

Similarity:

Václav Havel (1974)

Czechoslovak Mathematical Journal

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],...

Keppens, Dirk, Van Maldeghem, Hendrik (2009)

Beiträge zur Algebra und Geometrie

Similarity:

Roland Coghetto (2017)

Formalized Mathematics

Similarity:

Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group. Then, we prove that, using the notations of Borsuk and Szmielew in [3] “Consider in space ℝℙ2 points P1, P2, P3, P4 of which three points are not collinear and points Q1,Q2,Q3,Q4 each three points of which are also not collinear. There exists one homography h of space ℝℙ2 such that h(Pi) = Qi for i = 1, 2, 3, 4.” (Existence Statement 52 and Existence Statement 53)...

Claudio Bartolone, Fabio Di Franco (1979)

Mathematische Zeitschrift

Similarity: