Commit 2024-10-24 19:02 b8fa953f
View on Github →feat: Equivalence between OnePoint K and projective line over field K (#17266) Adding equivalence between OnePoint K and projective line over K, as discussed at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20Projective.20extended.20real.20line/near/463620378 The first PR for this became unable to automatically merge, so I am closing it and opening up this one. (I do have a proof extending this to a homeomorphism for K = Real, but perhaps it is more disciplined to do the Equiv first?)