Axiomatic projective geometry with morphisms

Stream: new members

[Abdullah Uyu]

Hello, I have been learning Lean for my graduation project, and a few weeks ago I finished the project. I set proving Desargues's Theorem as the end goal, but I couldn't reach to it. I learnt the basics of Lean, stated some basic definitions and proved some basic properties of the theory. I followed the book "Modern Projective Geometry". The source code of the repository is here: https://github.com/oneofvalts/desargues

Is this something that is useful to be in mathlib? Also, how can I improve the code?

[Yaël Dillies]

Yes it would certainly be in scope, although note that there are other projects around that. See https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Simple.20planar.20geometry

[Abdullah Uyu]

Ah, I wasn't subscribed to that channel, so I missed it. Thank you.