projective plane

Stream: new members

[Jenny Mason]

Hi I am new to lean and was wondering if anyone could suggest how I would go about constructing the 2 dim projective plane.

[Bryan Gin-ge Chen]

What construction were you thinking of formalizing?

[Kevin Buzzard]

Over an arbitrary field I guess $K$ I guess you could quotient out $K^3-\{(0,0,0)\}$ by the usual equivalence relation.