Timeline for Representing $\Bbb RP^2$ in Lean: building a type representing a particular set
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 12, 2022 at 22:13 | comment | added | John | Thanks. The first part of your answer is what I really needed; generalizing here makes it less useful, because this comes up in mimicking a development of projective geometry that only discusses $RP^2$ and $RP^3$ as examples, and doesn't have linear algebra as a prerequisite so much as a co-requisite. But the generalization is also interesting to me, so thanks for giving it! | |
| Feb 12, 2022 at 22:10 | vote | accept | John | ||
| S Feb 12, 2022 at 15:49 | review | First answers | |||
| Feb 12, 2022 at 15:59 | |||||
| S Feb 12, 2022 at 15:49 | history | answered | Adam Topaz | CC BY-SA 4.0 |