## Stream: new members

### Topic: projective plane

#### Jenny Mason (Oct 18 2018 at 14:33):

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 (Oct 18 2018 at 14:35):

What construction were you thinking of formalizing?

#### Kevin Buzzard (Oct 18 2018 at 15:06):

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

Last updated: May 12 2021 at 04:19 UTC