order — Mathlib

English

The order of a finite projective plane is one less than the number of lines through any point (equivalently, one less than the number of points on any line).

Русский

Порядок конечной проективной плоскости равен числу прямых через любую точку минус единицу (или числу точек на любую прямую минус единицу).

LaTeX

$$$\\text{order}(P,L) = \\text{lineCount}(L,p) - 1 = \\text{pointCount}(P,l) - 1$ for any point p and line l$$

Lean4

/-- The order of a projective plane is one less than the number of lines through an arbitrary point.
Equivalently, it is one less than the number of points on an arbitrary line. -/
noncomputable def order : ℕ :=
  lineCount L (Classical.choose (@exists_config P L _ _)) - 1

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