Zulip Chat Archive

Stream: new members

Topic: projective plane

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 14:35):

What construction were you thinking of formalizing?

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 15:06):

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

Last updated: May 12 2021 at 04:19 UTC