English
If P and L are finite with a projective plane of order n, then the number of points equals n^2 + n + 1.
Русский
Если плоскость порядка n, то число точек равно n^2 + n + 1.
LaTeX
$$$ |P| = (\operatorname{order} P L)^2 + (\operatorname{order} P L) + 1 $$$
Lean4
theorem card_points [Fintype P] [Finite L] : Fintype.card P = order P L ^ 2 + order P L + 1 :=
by
cases nonempty_fintype L
obtain ⟨p, -⟩ := @exists_config P L _ _
let ϕ : { q // q ≠ p } ≃ Σ l : { l : L // p ∈ l }, { q // q ∈ l.1 ∧ q ≠ p } :=
{ toFun := fun q => ⟨⟨mkLine q.2, (mkLine_ax q.2).2⟩, q, (mkLine_ax q.2).1, q.2⟩
invFun := fun lq => ⟨lq.2, lq.2.2.2⟩
right_inv := fun lq =>
Sigma.subtype_ext
(Subtype.ext ((eq_or_eq (mkLine_ax lq.2.2.2).1 (mkLine_ax lq.2.2.2).2 lq.2.2.1 lq.1.2).resolve_left lq.2.2.2))
rfl }
classical
have h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P :=
by
apply (eq_tsub_iff_add_eq_of_le (Nat.succ_le_of_lt (Fintype.card_pos_iff.mpr ⟨p⟩))).mp
convert (Fintype.card_subtype_compl _).trans (congr_arg _ (Fintype.card_subtype_eq p))
have h2 : ∀ l : { l : L // p ∈ l }, Fintype.card { q // q ∈ l.1 ∧ q ≠ p } = order P L :=
by
intro l
rw [← Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (· ∈ l.val) (· ≠ p)),
Fintype.card_subtype_compl fun x : Subtype (· ∈ l.val) => x.val = p, ← Nat.card_eq_fintype_card]
refine tsub_eq_of_eq_add ((pointCount_eq P l.1).trans ?_)
rw [← Fintype.card_subtype_eq (⟨p, l.2⟩ : { q : P // q ∈ l.1 })]
simp_rw [Subtype.ext_iff]
simp_rw [← h1, Fintype.card_congr ϕ, Fintype.card_sigma, h2, Finset.sum_const, Finset.card_univ]
rw [← Nat.card_eq_fintype_card, ← lineCount, lineCount_eq, smul_eq_mul, Nat.succ_mul, sq]
