card_lines — Mathlib

English

If P and L form a finite projective plane of order n, then the number of lines equals n^2 + n + 1.

Русский

Если плоскость порядка n, то число лучей равно n^2 + n + 1.

LaTeX

$$$ |L| = (\operatorname{order} P L)^2 + (\operatorname{order} P L) + 1 $$$

Lean4

theorem card_lines [Finite P] [Fintype L] : Fintype.card L = order P L ^ 2 + order P L + 1 :=
  (card_points (Dual L) (Dual P)).trans (congr_arg (fun n => n ^ 2 + n + 1) (Dual.order P L))

Похожие утверждения