Theorems · Definition · combinatorics
Configuration.ProjectivePlane.order
(P : Type u_1) → (L : Type u_2) → [inst : Membership P L] → [Configuration.ProjectivePlane P L] → ℕ
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.
- Defined in
- Mathlib.Combinatorics.Configuration
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Configuration.ProjectivePlanestatement and proof · cited by 14
- Configuration.lineCountproof · cited by 11
- Configuration.ProjectivePlane.exists_configproof · cited by 5
Cited by6
Results whose statement or proof uses this declaration.
- Configuration.ProjectivePlane.pointCount_eqstatement · cited by 3
- Configuration.ProjectivePlane.lineCount_eqstatement · cited by 3
- Configuration.ProjectivePlane.one_lt_orderstatement · cited by 2
- Configuration.ProjectivePlane.Dual.orderstatement · cited by 2
- Configuration.ProjectivePlane.card_pointsstatement and proof · cited by 1
- Configuration.ProjectivePlane.card_linesstatement · cited by 0