What is double cover

In this article, we will talk about double cover.

We will not discuss about $SU(2)$, $SO(3)$ or spinors, as there are enough videos on YouTube on this topic; you may pick your preferred flavor of education and watch them.

Here’s what I get from guessing, without reading any literature:

structure DoubleCover α where
  add : α -> α -> α
  zero : α
  a_turn : α
  add_zero : (x : α) -> add x zero = x
  double_cover : add a_turn a_turn = zero

Writing Lean feels right at home.

(this article is a placeholder for further extension)