WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Projective plane

Revision #2424 → #3107 · back to history

modifiedDual plane is a projective plane71e74246f4a2
FieldFrom #2424To #3107
mathlib.declConfiguration.ProjectivePlane.instProjectivePlaneDualConfiguration.ProjectivePlane.instDual
noteMathlib provides `instance : ProjectivePlane (Dual L) (Dual P)`, witnessing that the dual of a projective plane is a projective plane.Mathlib's `Configuration.ProjectivePlane.instDual` provides the `ProjectivePlane (Dual L) (Dual P)` instance, witnessing that the dual of a projective plane is a projective plane.
addedPoint-line incidence symmetry (order well-defined)a922faa057d1
addedFano plane PG(2,2)8ea7ff409ee6
addedHigher-dimensional projective space PG(d,K)7d538828f4ce