Skip to content

Erdős problem 723

Start work

If there is a finite projective plane of order nn then must nn be a prime power?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

723.lean

Retained formal statement1 of 5

If there is a finite projective plane of order nn then must nn be a prime power?

FormalConjectures/ErdosProblems/723.leanErdos723.erdos_7233 linesExact file
True ↔  ∀ {P L : Type} (x : Membership P L) (x_1 : Fintype P) (x_2 : Fintype L) (pp : Configuration.ProjectivePlane P L),    IsPrimePow (Configuration.ProjectivePlane.order P L)
OpenStatement only, no proof