Erdős problem 723
If there is a finite projective plane of order then must be a prime power?
Sources
FormalConjectures/ErdosProblems/
723.lean
Retained formal statement
If there is a finite projective plane of order then must be a prime power?
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