Structures · Combinatorics
Configuration.ProjectivePlane
A projective plane is a nondegenerate configuration in which every pair of lines has an intersection point, every pair of points has a line through them, and which has three points in general position.
- Defined in
- Mathlib.Combinatorics.Configuration
- Shape
- 2 explicit arguments · adds mkLine, mkLine_ax, exists_config
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Projectivization
- Configuration.Dual
How is a type an instance?
Loading the hierarchy index…
Assumed by19
- Configuration.ProjectivePlane.order
- Configuration.ProjectivePlane.exists_config
- Configuration.ProjectivePlane.lineCount_eq_lineCount
- Configuration.ProjectivePlane.pointCount_eq
- Configuration.ProjectivePlane.lineCount_eq
- Configuration.ProjectivePlane.one_lt_order
- Configuration.ProjectivePlane.card_points_eq_card_lines
- Configuration.ProjectivePlane.mkLine
- Configuration.ProjectivePlane.Dual.order
- Configuration.ProjectivePlane.lineCount_eq_pointCount
- Configuration.ProjectivePlane.mkLine_ax
- Configuration.ProjectivePlane.card_points
- Configuration.ProjectivePlane.pointCount_eq_pointCount
- Configuration.ProjectivePlane.instDual
- Configuration.ProjectivePlane.toHasLines
- Configuration.ProjectivePlane.toHasPoints
- Configuration.ProjectivePlane.card_lines
- Configuration.ProjectivePlane.two_lt_lineCount
- Configuration.ProjectivePlane.two_lt_pointCount