Skip to content

Commit

Permalink
Make a start on Spin groups as an article
Browse files Browse the repository at this point in the history
  • Loading branch information
utensil committed Apr 30, 2024
1 parent 4a90060 commit 67bba9c
Show file tree
Hide file tree
Showing 4 changed files with 33 additions and 4 deletions.
7 changes: 7 additions & 0 deletions templates/block.tree
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
\import{macros}

\block{}{



}
12 changes: 8 additions & 4 deletions trees/spin-0001.tree
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,13 @@

\date{2024-04-26}

\p{This survey is built on my notes in the process of figuring out [[ericwieser]]'s MathOverflow question [Definition of a spin group](https://mathoverflow.net/questions/427881/definition-of-a-spin-group) for [our PR to Mathlib4 about Spin groups](https://github.com/leanprover-community/mathlib4/pull/9111/).}
\transclude{spin-000R}

\p{This is also my first [[uts-0001]].}
\transclude{spin-000S}

\p{Now it's a work-in-progress. Definitions coming from different sources are simply quoted here with minimal modifications, to include immediate prerequisites, and omit some discussions or theorems. Definitions that are too similar are not yet pruned. And the order is quite arbitrary at the moment.}
\block{Appendix: definitions of Spin group from various source}{

\p{Definitions coming from different sources are simply quoted here with minimal modifications, to include immediate prerequisites, and omit some discussions or theorems. Definitions that are too similar are not pruned. The order is quite arbitrary.}

\transclude{spin-0002}

Expand Down Expand Up @@ -65,4 +67,6 @@

\transclude{spin-000P}

\transclude{spin-000Q}
\transclude{spin-000Q}

}
7 changes: 7 additions & 0 deletions trees/spin-000R.tree
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
\import{macros}

\title{Motivation}

\p{This survey is built on my notes in the process of figuring out [[ericwieser]]'s MathOverflow question [Definition of a spin group](https://mathoverflow.net/questions/427881/definition-of-a-spin-group) for [our PR to Mathlib4 about Spin groups](https://github.com/leanprover-community/mathlib4/pull/9111/).}

\p{This is also my first [[uts-0001]].}
11 changes: 11 additions & 0 deletions trees/spin-000S.tree
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
\import{macros}

\title{Status}

\p{Currently it's a work-in-progress.}

\p{TODO}

\ul{
\li{classify them by the prerequisites, style, and similarity}
}

0 comments on commit 67bba9c

Please sign in to comment.