Number of points of a finite projective plane

Remarks

Fix a point $P$. It lies on $n + 1$ lines, and each of them has $n$ points other than $P$. Every other point $Q$ lies on exactly one line through $P$, namely $PQ$, so the number of points is $1 + (n + 1) n = n^2 + n + 1$. The count of lines follows by the same argument in the dual plane, which is again a projective plane of order $n$.

Example: the Fano plane has order $2$ and $4 + 2 + 1 = 7$ points. The plane $PG(2, q)$ has $(q^3 - 1)/(q - 1) = q^2 + q + 1$ points, as it should. In Mathlib the count of points is Configuration.ProjectivePlane.card_points.

Going deeper

For a student

The proof is a standard double count from a single point, and the same method gives the counts of flags and of triangles. It shows that a projective plane of order $n$ is a symmetric block design with parameters $(n^2 + n + 1, n + 1, 1)$, a Steiner system $S(2, n + 1, n^2 + n + 1)$. This turns existence questions for planes into questions about designs, which is the setting of the Bruck–Ryser–Chowla theorem.